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