let SAS be Semi_Affine_Space; :: thesis: for a, b, o, x being Element of SAS st not o,a,b are_collinear & o,a,x are_collinear & o,b,x are_collinear holds
o = x
let a, b, o, x be Element of SAS; :: thesis: ( not o,a,b are_collinear & o,a,x are_collinear & o,b,x are_collinear implies o = x )
assume that
A1: not o,a,b are_collinear and
A2: o,a,x are_collinear and
A3: o,b,x are_collinear ; :: thesis: o = x
b,o,x are_collinear by A3, Th22;
then A4: b,o // b,x ;
o,a // o,x by A2;
then A5: a,o // a,x by Th14;
not a,b,o are_collinear by A1, Th22;
then not a,b // a,o ;
hence o = x by A5, A4, Th18; :: thesis: verum