set M = finite-MultiSet_over the carrier of R;
defpred S₁[ bag of the carrier of R, bag of the carrier of R] means ex x, y being Element of (finite-MultiSet_over the carrier of R) st
( 1. (finite-MultiSet_over the carrier of R) <> x & x divides $2 & $1 = ($2 -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) );
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 ex x, y being Element of N st
( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) )
let m, n be Element of N; :: thesis: ( m <= n iff ex x, y being Element of N st
( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) )

hereby :: thesis: ( ex x, y being Element of N st
( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) implies m <= n )

assume m <= n ; :: thesis: ex x, y being Element of N st
( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) )
then consider x, y being Element of (finite-MultiSet_over the carrier of R) such that
A2: ( 1. (finite-MultiSet_over the carrier of R) <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by A1;
reconsider x = x, y = y as Element of N by Th2;
take x = x; :: thesis: ex y being Element of N st
( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) )
take y = y; :: thesis: ( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) )
thus ( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by A2, Th3; :: thesis: verum

end;

given x, y being Element of N such that A3: ( 1. N <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ; :: thesis: m <= n
reconsider x = x, y = y as Element of (finite-MultiSet_over the carrier of R) by Th2;
( 1. (finite-MultiSet_over the carrier of R) <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by A3, Th3;
hence m <= n by A1; :: thesis: verum