assume [A,B,C,D,A1,B1,C1,D1] : (point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & point(C1) & point(D1) & ifs(A,B,C,D,A1,B1,C1,D1))

disjunction (A = C | A != C)

suppose (A = C)

have (A1 = C1)
have (B = C & B1 = C1)
show (cong(B,C,B1,D1))

suppose (A != C)

let [E] : (point(E) & bet(A,C,E) & C != E)
let [E1] : (point(E1) & bet(A1,C1,E1) & cong(C1,E1,C,E))
have (afs(A,C,E,D,A1,C1,E1,D1))
have (cong(E,D,E1,D1))
have (afs(E,C,B,D,E1,C1,B1,D1))
show (cong(B,D,B1,D1))

end_disjunction
