let SAS be Semi_Affine_Space; :: thesis: for a, b, c, x being Element of SAS st a,b // a,x & b,c // b,x & c,a // c,x holds
a,b // a,c
let a, b, c, x be Element of SAS; :: thesis: ( a,b // a,x & b,c // b,x & c,a // c,x implies a,b // a,c )
assume that
A1: a,b // a,x and
A2: b,c // b,x and
A3: c,a // c,x ; :: thesis: a,b // a,c

now :: thesis: ( a <> x implies a,b // a,c )

assume A4: a <> x ; :: thesis: a,b // a,c
( a,x // a,b & a,x // a,c ) by A1, A3, Th7;
hence a,b // a,c by A4, Def1; :: thesis: verum

end;

hence a,b // a,c by A2, Th7; :: thesis: verum