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 )
assume A2: ( 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
A3: not b,a // b,c by A1, Th18;

now

assume a,c // c,b ; :: thesis: contradiction
then c,a // c,b by Th17;
hence contradiction by A1, Th18; :: thesis: verum

end;

hence contradiction by A1, A2, A3, Th17; :: thesis: verum