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 ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) ) & ( for m, n being Element of N2 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) ) implies N1 = N2 )
assume that
A1: for m, n being Element of N1 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) and
A2: for m, n being Element of N2 holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) ; :: 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 ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) by A1;
hence ( m <= n iff k <= l ) by A2, Z0, Z1; :: thesis: verum

end;

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