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 a' = a, b' = b, c' = c, d' = d as Element of (Af 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: a',b' // c',d' by Th48;
then A2: ( b',a' // d',c' & c',d' // a',b' ) by AFF_1:13;
A3: d',c' // b',a' by A1, AFF_1:13;
A4: ( c',d' // b',a' & d',c' // a',b' ) by A1, AFF_1:13;
( a',b' // d',c' & b',a' // c',d' ) by A1, 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 A2, A4, A3, Th48; :: thesis: verum