let OTS be OrdTrapSpace; :: thesis: for a1', b1', a', b', c', d' being Element of 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 ; :: thesis: ( a1' <> b1' & a1',b1' // a',b' & a1',b1' // c',d' implies a',b' // c',d' )
reconsider a1 = a1', b1 = b1', a = a', b = b', c = c', d = d' as Element of by Th50;
assume that
A1: a1' <> b1' and
A2: a1',b1' // a',b' and
A3: a1',b1' // c',d' ; :: thesis: a',b' // c',d'
A4: ( a1,b1 // c,d or a1,b1 // d,c ) by A3, Th51;
( a1,b1 // a,b or a1,b1 // b,a ) 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, A4, Def14;
then ( a,b // c,d or a,b // d,c ) by Def14;
hence a',b' // c',d' by Th51; :: thesis: verum