set I = the carrier of R;
set M = finite-MultiSet_over the carrier of R;
defpred S₁[ bag of the carrier of R, bag of the carrier of R] means ( $1 <> $2 & ( for x being Element of R holds
( not $1 . x > 0 or $1 . x < $2 . x or ex y being Element of R st
( $2 . y > 0 & x <= y ) ) ) );
consider N being strict RelExtension of finite-MultiSet_over the carrier of R such that
A1: for m, n being Element of N holds
( m <= n iff S₁[m,n] ) from BAGORD_2:sch 1();
take N ; :: thesis: for m, n being Element of N 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 ) ) ) ) )
thus for m, n being Element of N 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 ) ) ) ) ) by A1; :: thesis: verum