let OTS be OrdTrapSpace; :: thesis: for a1', b1', a', b', c', d' being Element of (Lambda OTS) st a1' <> b1' & a1',b1' // a',b' & a1',b1' // c',d' holds
a',b' // c',d'
let a1', b1', a', b', c', d' be Element of (Lambda OTS); :: thesis: ( a1' <> b1' & a1',b1' // a',b' & a1',b1' // c',d' implies a',b' // c',d' )
assume that
A1: a1' <> b1' and
A2: ( a1',b1' // a',b' & a1',b1' // c',d' ) ; :: thesis: a',b' // c',d'
reconsider a1 = a1', b1 = b1', a = a', b = b', c = c', d = d' as Element of OTS by Th50;
( ( a1,b1 // a,b or a1,b1 // b,a ) & ( a1,b1 // c,d or a1,b1 // d,c ) ) by A2, Th51;
then ( a,b // c,d or a,b // d,c or b,a // c,d or b,a // d,c ) by A1, Def14;
then ( a,b // c,d or a,b // d,c ) by Def14;
hence a',b' // c',d' by Th51; :: thesis: verum