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))
have (cong(B,D,B1,D1))

