let POS be OrtAfSp; :: thesis: for a, b, c, d being Element of POS st a,b // c,d holds
( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a )
let a, b, c, d be Element of POS; :: thesis: ( a,b // c,d implies ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
assume a,b // c,d ; :: thesis: ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a )
then A1: a9,b9 // c9,d9 by Th36;
then A2: ( b9,a9 // d9,c9 & c9,d9 // a9,b9 ) by AFF_1:4;
A3: d9,c9 // b9,a9 by A1, AFF_1:4;
A4: ( c9,d9 // b9,a9 & d9,c9 // a9,b9 ) by A1, AFF_1:4;
( a9,b9 // d9,c9 & b9,a9 // c9,d9 ) by A1, AFF_1:4;
hence ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a ) by A2, A4, A3, Th36; :: thesis: verum