set R = DivOrder I;
now for x, y being object st [x,y] in DivOrder I holds
not [y,x] in DivOrder Ilet x,
y be
object ;
( [x,y] in DivOrder I implies not [y,x] in DivOrder I )assume A1:
[x,y] in DivOrder I
;
not [y,x] in DivOrder Ithen 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;
verum end;
hence
DivOrder I is asymmetric
by PREFER_1:22; DivOrder I is transitive
let a, b, c be object ; RELAT_2:def 8,RELAT_2:def 16 ( 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) )
; ( 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 )
; [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; verum