let SAS be Semi_Affine_Space; :: thesis: 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
let a, b, c, d, p1, p2 be Element of SAS; :: thesis: ( 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 implies p1 = p2 )
assume that
A1: not a,b // c,d and
A2: ( a,b,p1 are_collinear & a,b,p2 are_collinear ) and
A3: ( c,d,p1 are_collinear & c,d,p2 are_collinear ) ; :: thesis: p1 = p2
c,d // p1,p2 by A3, Th26;
then A4: p1,p2 // c,d by Th6;
a,b // p1,p2 by A2, Th26;
then p1,p2 // a,b by Th6;
hence p1 = p2 by A1, A4, Def1; :: thesis: verum