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

A2: now

assume 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;

now

assume 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;

hence c',d' // a',b' by A1, A2, Th51; :: thesis: verum