defpred S₁[ set , set ] means ex b1, b2 being Element of Bags n st
( $1 = b1 & $2 = b2 & b1 <=' b2 );
consider BO being Relation of (Bags n),(Bags n) such that
A1: for x, y being set holds
( [x,y] in BO iff ( x in Bags n & y in Bags n & S₁[x,y] ) ) from RELSET_1:sch 1();
A2: BO is_reflexive_in Bags n

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in Bags n or [x,x] in BO )
assume x in Bags n ; :: thesis: [x,x] in BO
hence [x,x] in BO by A1; :: thesis: verum

end;

A3: BO is_antisymmetric_in Bags n

proof

let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in Bags n or not y in Bags n or not [x,y] in BO or not [y,x] in BO or x = y )
assume A4: ( x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO ) ; :: thesis: x = y
then consider b1, b2 being Element of Bags n such that
A5: ( x = b1 & y = b2 & b1 <=' b2 ) by A1;
consider b1', b2' being Element of Bags n such that
A6: ( y = b1' & x = b2' & b1' <=' b2' ) by A1, A4;
( ( b1 < b2 or b1 = b2 ) & ( b1' < b2' or b1' = b2' ) ) by A5, A6, Def12;
hence x = y by A5, A6; :: thesis: verum

end;

A7: BO is_transitive_in Bags n

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in Bags n or not y in Bags n or not z in Bags n or not [x,y] in BO or not [y,z] in BO or [x,z] in BO )
assume that
( x in Bags n & y in Bags n & z in Bags n ) and
A8: ( [x,y] in BO & [y,z] in BO ) ; :: thesis: [x,z] in BO
consider b1, b2 being Element of Bags n such that
A9: ( x = b1 & y = b2 & b1 <=' b2 ) by A1, A8;
consider b1', b2' being Element of Bags n such that
A10: ( y = b1' & z = b2' & b1' <=' b2' ) by A1, A8;
reconsider B1 = b1, B2' = b2' as bag of ;
B1 <=' B2' by A9, A10, Th46;
hence [x,z] in BO by A1, A9, A10; :: thesis: verum

end;

( dom BO = Bags n & field BO = Bags n ) by A2, ORDERS_1:98;
then reconsider BO = BO as Order of (Bags n) by A2, A3, A7, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take BO ; :: thesis: for p, q being bag of holds
( [p,q] in BO iff p <=' q )
let p, q be bag of ; :: thesis: ( [p,q] in BO iff p <=' q )
A11: ( p in Bags n & q in Bags n ) by Def14;

hereby :: thesis: ( p <=' q implies [p,q] in BO )

assume [p,q] in BO ; :: thesis: p <=' q
then consider b1, b2 being Element of Bags n such that
A12: ( p = b1 & q = b2 & b1 <=' b2 ) by A1;
thus p <=' q by A12; :: thesis: verum

end;

thus ( p <=' q implies [p,q] in BO ) by A1, A11; :: thesis: verum