let OTS be OrdTrapSpace; :: thesis: for a9, b9, c9, d9, a19, b19 being Element of (Lambda OTS) st a19 <> b19 & a19,b19 // a9,b9 & a19,b19 // c9,d9 holds
a9,b9 // c9,d9
let a9, b9, c9, d9, a19, b19 be Element of (Lambda OTS); :: thesis: ( a19 <> b19 & a19,b19 // a9,b9 & a19,b19 // c9,d9 implies a9,b9 // c9,d9 )
reconsider a1 = a19, b1 = b19, a = a9, b = b9, c = c9, d = d9 as Element of OTS by Th47;
assume that
A1: a19 <> b19 and
A2: a19,b19 // a9,b9 and
A3: a19,b19 // c9,d9 ; :: thesis: a9,b9 // c9,d9
A4: ( a1,b1 // c,d or a1,b1 // d,c ) by A3, Th48;
( a1,b1 // a,b or a1,b1 // b,a ) by A2, Th48;
then ( a,b // c,d or a,b // d,c or b,a // c,d or b,a // d,c ) by A1, A4, Def12;
then ( a,b // c,d or a,b // d,c ) by Def12;
hence a9,b9 // c9,d9 by Th48; :: thesis: verum