let SAS be Semi_Affine_Space; :: thesis: for o, a, c, b, d1, d2 being Element of SAS st not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d2 holds
d1 = d2
let o, a, c, b, d1, d2 be Element of SAS; :: thesis: ( not o,a,c is_collinear & o,a,b is_collinear & o,c,d1 is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d2 implies d1 = d2 )
assume that
A1: ( not o,a,c is_collinear & o,a,b is_collinear ) and
A2: ( o,c,d1 is_collinear & o,c,d2 is_collinear ) and
A3: ( a,c // b,d1 & a,c // b,d2 ) ; :: thesis: d1 = d2
A4: ( o,c // o,d1 & o,c // o,d2 ) by A2, Def2;
( not o,a // o,c & o,a // o,b ) by A1, Def2;
hence d1 = d2 by A3, A4, Th33; :: thesis: verum