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