assume [A,B,C0,C1] : (point(A) & point(B) & point(C0) & point(C1) & A!=B & C0!=C1 & cong_less(C0,C1,A,B))
construct [D] : (point(D) & cong(A,D,C0,C1))
construct [K] : (circle(K) & center(A,K) & onc(D,K))
construct [L] : (line(L) & on(A,L) & on(B,L))
construct [E] : (point(E) & onc(E,K) & on(E,L) & bet(A,E,B))
infer (cong(A,D,A,E))
infer (cong(A,E,C0,C1))
