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 that
A1: not o,a,b is_collinear and
A2: o,a,x is_collinear and
A3: o,b,x is_collinear ; :: thesis: o = x
b,o,x is_collinear by A3, Th37;
then A4: b,o // b,x by Def2;
o,a // o,x by A2, Def2;
then A5: a,o // a,x by Th28;
not a,b,o is_collinear by A1, Th37;
then not a,b // a,o by Def2;
hence o = x by A5, A4, Th32; :: thesis: verum