let PS be ParSp; :: thesis: for a, b, c being Element of PS st not a,b '||' a,c holds
( not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c )
let a, b, c be Element of PS; :: thesis: ( not a,b '||' a,c implies ( not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c ) )
assume A1: not a,b '||' a,c ; :: thesis: ( not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c )
assume ( a,c '||' a,b or b,a '||' a,c or a,b '||' c,a or a,c '||' b,a or b,a '||' c,a or c,a '||' a,b or c,a '||' b,a or b,a '||' b,c or a,b '||' b,c or b,a '||' c,b or b,c '||' b,a or b,a '||' c,b or c,b '||' b,a or b,c '||' a,b or c,b '||' a,b or c,a '||' c,b or a,c '||' c,b or c,a '||' b,c or a,c '||' b,c or c,b '||' c,a or b,c '||' c,a or c,b '||' a,c or b,c '||' a,c ) ; :: thesis: contradiction
then ( a,c '||' a,b or a,b '||' a,c or a,b '||' a,c or a,c '||' a,b or a,b '||' a,c or a,c '||' a,b or a,c '||' a,b or b,a '||' b,c or b,a '||' b,c or b,a '||' b,c or b,c '||' b,a or b,a '||' b,c or b,c '||' b,a or b,c '||' b,a or b,c '||' b,a or c,a '||' c,b or c,a '||' c,b or c,a '||' c,b or c,a '||' c,b or c,b '||' c,a or c,b '||' c,a or c,b '||' c,a or c,b '||' c,a ) by Th23;
hence contradiction by A1, Th24; :: thesis: verum