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)

case (A = C)

infer (A1 = C1)
infer (B = C & B1 = C1)
lookup (cong(B,C,B1,D1))

case (A != C)

construct [E] : (point(E) & bet(A,C,E) & C != E)
construct [E1] : (point(E1) & bet(A1,C1,E1) & cong(C1,E1,C,E))
infer (afs(A,C,E,D,A1,C1,E1,D1))
infer (cong(E,D,E1,D1))
infer (afs(E,C,B,D,E1,C1,B1,D1))
lookup (cong(B,D,B1,D1))

end_disjunction
