let SAS be Semi_Affine_Space; 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; ( 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
; ( 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 not a,c // c,bassume
a,
c // c,
b
;
contradictionthen
c,
a // c,
b
by Th6;
hence
contradiction
by A1, Th7;
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 )
; contradiction
not b,a // b,c
by A1, Th7;
hence
contradiction
by A1, A3, A2, Th6; verum