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