for SAS being Semi_Affine_Space
for a, b, c, d, p1, p2 being Element of SAS st not a,b // c,d & a,b,p1 are_collinear & a,b,p2 are_collinear & c,d,p1 are_collinear & c,d,p2 are_collinear holds
p1 = p2