let N1, N2 be strict RelExtension of finite-MultiSet_over the carrier of R; :: thesis: ( ( for m, n being Element of N1 holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) ) & ( for m, n being Element of N2 holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) ) implies N1 = N2 )
assume that
A1: for m, n being Element of N1 holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) and
A2: for m, n being Element of N2 holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) ; :: thesis: N1 = N2
for m, n being Element of N1
for x, y being Element of N2 st m = x & n = y holds
( m <= n iff x <= y )

proof

let m, n be Element of N1; :: thesis: for x, y being Element of N2 st m = x & n = y holds
( m <= n iff x <= y )
let k, l be Element of N2; :: thesis: ( m = k & n = l implies ( m <= n iff k <= l ) )
assume Z0: m = k ; :: thesis: ( not n = l or ( m <= n iff k <= l ) )
assume Z1: n = l ; :: thesis: ( m <= n iff k <= l )
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) by A1;
hence ( m <= n iff k <= l ) by A2, Z0, Z1; :: thesis: verum

end;

hence N1 = N2 by Th4; :: thesis: verum