let OTS be OrdTrapSpace; :: thesis: for a', b', c', d' being Element of st a',b' // c',d' holds
c',d' // a',b'
let a', b', c', d' be Element of ; :: thesis: ( a',b' // c',d' implies c',d' // a',b' )
reconsider a = a', b = b', c = c', d = d' as Element of the carrier of OTS by Th50;
assume A1: a',b' // c',d' ; :: thesis: c',d' // a',b'

per cases ( a,b // c,d or a,b // d,c ) by A1, Th51;

suppose a,b // c,d ; :: thesis: c',d' // a',b'

then c,d // a,b by Def14;
hence c',d' // a',b' by Th51; :: thesis: verum

end;

suppose a,b // d,c ; :: thesis: c',d' // a',b'

then b,a // c,d by Def14;
then c,d // b,a by Def14;
hence c',d' // a',b' by Th51; :: thesis: verum

end;

end;