defpred S1[ 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 & S1[x,y] ) )
from RELSET_1:sch 1();
A2:
BO is_transitive_in Bags n
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( 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
;
[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;
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 ;
RELAT_2:def 4 ( 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
;
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 ;
dom b11 =
n
by PARTFUN1:def 2
.=
dom b22
by PARTFUN1:def 2
;
hence
x = y
by A16, A18, FUNCT_1:2;
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
; for b1, b2 being bag of n holds
( [b1,b2] in BO iff b1 divides b2 )
let p, q be bag of n; ( [p,q] in BO iff p divides q )
( p in Bags n & q in Bags n )
by PRE_POLY:def 12;
hence
( p divides q implies [p,q] in BO )
by A1; verum