defpred S₁[ set , set ] means ex b1, b2 being Element of Bags n st
( $1 = b1 & $2 = b2 & b1 divides 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 b11, b22 being Element of Bags n such that
A5: ( x = b11 & y = b22 & b11 divides b22 ) by A1;
consider b1', b2' being Element of Bags n such that
A6: ( y = b1' & x = b2' & b1' divides b2' ) by A1, A4;
reconsider b11 = b11, b22 = b22 as bag of ;
A7: dom b11 = n by PARTFUN1:def 4
.= dom b22 by PARTFUN1:def 4 ;

now

let k be set ; :: thesis: ( k in dom b11 implies b11 . k = b22 . k )
assume k in dom b11 ; :: thesis: b11 . k = b22 . k
A8: b11 . k <= b22 . k by A5, POLYNOM1:def 13;
b1' . k <= b2' . k by A6, POLYNOM1:def 13;
hence b11 . k = b22 . k by A5, A6, A8, XXREAL_0:1; :: thesis: verum

end;

hence x = y by A5, A7, FUNCT_1:9; :: thesis: verum

end;

A9: 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
A10: ( [x,y] in BO & [y,z] in BO ) ; :: thesis: [x,z] in BO
consider b1, b2 being Element of Bags n such that
A11: ( x = b1 & y = b2 & b1 divides b2 ) by A1, A10;
consider b11, b22 being Element of Bags n such that
A12: ( y = b11 & z = b22 & b11 divides b22 ) by A1, A10;
reconsider B1 = b1, B2' = b22 as bag of ;
B1 divides B2' by A11, A12, Lm8;
hence [x,z] in BO by A1, A11, A12; :: 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, A9, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take BO ; :: thesis: for b1, b2 being bag of holds
( [b1,b2] in BO iff b1 divides b2 )
let p, q be bag of ; :: thesis: ( [p,q] in BO iff p divides q )
A13: ( p in Bags n & q in Bags n ) by POLYNOM1:def 14;

hereby :: thesis: ( p divides q implies [p,q] in BO )

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

end;

thus ( p divides q implies [p,q] in BO ) by A1, A13; :: thesis: verum