defpred S₁[ object , object ] 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 object 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_transitive_in Bags n

proof

let x, y, z be object ; :: 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 and
y in Bags n and
z in Bags n and
A3: [x,y] in BO and
A4: [y,z] in BO ; :: thesis: [x,z] in BO
consider b1, b2 being Element of Bags n such that
A5: x = b1 and
A6: ( y = b2 & b1 divides b2 ) by A1, A3;
consider b11, b22 being Element of Bags n such that
A7: y = b11 and
A8: z = b22 and
A9: b11 divides b22 by A1, A4;
reconsider B1 = b1, B29 = b22 as bag of n ;
B1 divides B29 by A6, A7, A9, Lm8;
hence [x,z] in BO by A1, A5, A8; :: thesis: verum

end;

A10: BO is_reflexive_in Bags n by A1;
then A11: ( dom BO = Bags n & field BO = Bags n ) by ORDERS_1:13;
BO is_antisymmetric_in Bags n

proof

let x, y be object ; :: 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 that
x in Bags n and
y in Bags n and
A12: [x,y] in BO and
A13: [y,x] in BO ; :: thesis: x = y
consider b19, b29 being Element of Bags n such that
A14: ( y = b19 & x = b29 ) and
A15: b19 divides b29 by A1, A13;
consider b11, b22 being Element of Bags n such that
A16: ( x = b11 & y = b22 ) and
A17: b11 divides b22 by A1, A12;
reconsider b11 = b11, b22 = b22 as bag of n ;

A18: now :: thesis: for k being object st k in dom b11 holds
b11 . k = b22 . k

let k be object ; :: thesis: ( k in dom b11 implies b11 . k = b22 . k )
assume k in dom b11 ; :: thesis: b11 . k = b22 . k
( b11 . k <= b22 . k & b19 . k <= b29 . k ) by A17, A15, PRE_POLY:def 11;
hence b11 . k = b22 . k by A16, A14, XXREAL_0:1; :: thesis: verum

end;

dom b11 = n by PARTFUN1:def 2
.= dom b22 by PARTFUN1:def 2 ;
hence x = y by A16, A18, FUNCT_1:2; :: thesis: verum

end;

then reconsider BO = BO as Order of (Bags n) by A10, A2, A11, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take BO ; :: thesis: for b1, b2 being bag of n holds
( [b1,b2] in BO iff b1 divides b2 )
let p, q be bag of n; :: thesis: ( [p,q] in BO iff p divides q )

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

assume [p,q] in BO ; :: thesis: p divides q
then ex b19, b29 being Element of Bags n st
( p = b19 & q = b29 & b19 divides b29 ) by A1;
hence p divides q ; :: thesis: verum

end;

( p in Bags n & q in Bags n ) by PRE_POLY:def 12;
hence ( p divides q implies [p,q] in BO ) by A1; :: thesis: verum