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 [(OrderedPartition $1),(OrderedPartition $2)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R));
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 [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) )
thus for m, n being Element of N holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) by A1; :: thesis: verum