let SAS be Semi_Affine_Space; :: thesis: for o, a, b, x being Element of SAS st not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear holds
o = x
let o, a, b, x be Element of SAS; :: thesis: ( not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear implies o = x )
assume ( not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear ) ; :: thesis: o = x
then ( not a,b,o is_collinear & o,a,x is_collinear & b,o,x is_collinear ) by Th37;
then ( not a,b // a,o & o,a // o,x & b,o // b,x ) by Def2;
then ( not a,b // a,o & a,o // a,x & b,o // b,x ) by Th28;
hence o = x by Th32; :: thesis: verum