assume [A,B,C,D,E,F] : (point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & ncol(A,B,C) & A!=B & A!=C & B!=C & ncol(D,E,F) & D!=E & E!=F & F!=D & cong(A,B,D,E) & cong(A,C,D,F) & cong_angle(B,A,C,E,D,F))
let [L] : (line(L) & on(D,L) & on(E,L))
have (non(F,L))
let [B1,C1] : (point(B1) & point(C1) & cong_angle(B,A,C,B1,D,C1) & cong_angle(A,C,B,D,C1,B1) & cong_angle(C,B,A,C1,B1,D) & cong(A,B,D,B1) & cong(B,C,B1,C1) & cong(C,A,C1,D) & on(B1,L) & nbet(B1,D,E) & sameside(C1,F,L) & B1!=C1 & D!=C1)
have (cong_zero(B1,E))
have (B1=E)
have (cong_angle(E,D,C1,E,D,F))
have (cong(D,C1,D,F))
have (cong_zero(C1,F))
have (C1=F)
have (cong(B,C,E,F) & cong_angle(A,B,C,D,E,F) & cong_angle(A,C,B,D,F,E))
