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 ) )
assume A1: 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 )
reconsider a' = a, b' = b, c' = c, d' = d as Element of the carrier of (Af POS) ;
a',b' // c',d' by A1, Th48;
then ( 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 AFF_1:13;
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 Th48; :: thesis: verum