set R = DivOrder I;

now :: thesis: for x, y being object st [x,y] in DivOrder I holds
not [y,x] in DivOrder I

let x, y be object ; :: thesis: ( [x,y] in DivOrder I implies not [y,x] in DivOrder I )
assume A1: [x,y] in DivOrder I ; :: thesis: not [y,x] in DivOrder I
then reconsider a = x, b = y as Element of Bags I by ZFMISC_1:87;
A2: ( a <> b & a divides b ) by DO, A1;
then consider o being object such that
A3: ( o in I & a . o <> b . o ) by PBOOLE:def 10;
a . o <= b . o by A2, PRE_POLY:def 11;
then a . o < b . o by A3, XXREAL_0:1;
then not b divides a by PRE_POLY:def 11;
hence not [y,x] in DivOrder I by DO; :: thesis: verum

end;

hence DivOrder I is asymmetric by PREFER_1:22; :: thesis: DivOrder I is transitive
let a, b, c be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not a in field (DivOrder I) or not b in field (DivOrder I) or not c in field (DivOrder I) or not [a,b] in DivOrder I or not [b,c] in DivOrder I or [a,c] in DivOrder I )
assume ( a in field (DivOrder I) & b in field (DivOrder I) & c in field (DivOrder I) ) ; :: thesis: ( not [a,b] in DivOrder I or not [b,c] in DivOrder I or [a,c] in DivOrder I )
assume A4: ( [a,b] in DivOrder I & [b,c] in DivOrder I ) ; :: thesis: [a,c] in DivOrder I
then reconsider a = a, b = b, c = c as Element of Bags I by ZFMISC_1:87;
A5: ( a <> b & a divides b & b divides c ) by A4, DO;
then consider x being object such that
A6: ( x in I & a . x <> b . x ) by PBOOLE:def 10;
a . x <= b . x by A5, PRE_POLY:def 11;
then ( a . x < b . x & b . x <= c . x ) by A5, A6, XXREAL_0:1, PRE_POLY:def 11;
then ( a <> c & a divides c ) by A5, Lem7;
hence [a,c] in DivOrder I by DO; :: thesis: verum