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

A2: now :: thesis: not a,c // c,b

assume a,c // c,b ; :: thesis: contradiction
then c,a // c,b by Th6;
hence contradiction by A1, Th7; :: thesis: verum

end;

assume A3: ( a,b // c,a or b,a // a,c or b,a // c,a or a,c // a,b or a,c // b,a or c,a // a,b or c,a // b,a or b,a // b,c or b,a // c,b or a,b // b,c or a,b // c,b or b,c // b,a or b,c // a,b or c,b // a,b or c,b // b,a or c,b // c,a or c,b // a,c or b,c // c,a or b,c // a,c or c,a // c,b or c,a // b,c or a,c // b,c or a,c // c,b ) ; :: thesis: contradiction
not b,a // b,c by A1, Th7;
hence contradiction by A1, A3, A2, Th6; :: thesis: verum