let OTS be OrdTrapSpace; :: thesis: for a19, b19, a9, b9, c9, d9 being Element of (Lambda OTS) st a19 <> b19 & a19,b19 // a9,b9 & a19,b19 // c9,d9 holds
a9,b9 // c9,d9
let a19, b19, a9, b9, c9, d9 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 Th50;
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, 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 a9,b9 // c9,d9 by Th51; :: thesis: verum