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