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,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,d1 & a,c // b,d2 implies d1 = d2 )
assume ( 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,d1 & a,c // b,d2 ) ; :: thesis: d1 = d2
then ( not o,a // o,c & o,a // o,b & o,c // o,d1 & o,c // o,d2 & a,c // b,d1 & a,c // b,d2 ) by Def2;
hence d1 = d2 by Th33; :: thesis: verum