let SAS be Semi_Affine_Space; 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; ( 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
; a,b // a,c
now ( a <> x implies a,b // a,c )assume A4:
a <> x
;
a,b // a,c
(
a,
x // a,
b &
a,
x // a,
c )
by A1, A3, Th7;
hence
a,
b // a,
c
by A4, Def1;
verum end;
hence
a,b // a,c
by A2, Th7; verum