defpred S1[ object , object ] means ex b1, b2 being Element of Bags n st
( $1 = b1 & $2 = b2 & b1 <=' 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_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 A3:
[x,y] in BO
and A4:
[y,x] in BO
;
x = y
A5:
ex
b19,
b29 being
Element of
Bags n st
(
y = b19 &
x = b29 &
b19 <=' b29 )
by A1, A4;
consider b1,
b2 being
Element of
Bags n such that A6:
(
x = b1 &
y = b2 )
and A7:
b1 <=' b2
by A1, A3;
(
b1 < b2 or
b1 = b2 )
by A7;
hence
x = y
by A6, A5;
verum
end;
A8:
BO is_reflexive_in Bags n
by A1;
then A9:
( dom BO = Bags n & field BO = Bags n )
by ORDERS_1:13;
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 A10:
[x,y] in BO
and A11:
[y,z] in BO
;
[x,z] in BO
consider b1,
b2 being
Element of
Bags n such that A12:
x = b1
and A13:
(
y = b2 &
b1 <=' b2 )
by A1, A10;
consider b19,
b29 being
Element of
Bags n such that A14:
y = b19
and A15:
z = b29
and A16:
b19 <=' b29
by A1, A11;
reconsider B1 =
b1,
B29 =
b29 as
bag of
n ;
B1 <=' B29
by A13, A14, A16, Th41;
hence
[x,z] in BO
by A1, A12, A15;
verum
end;
then reconsider BO = BO as Order of (Bags n) by A8, A2, A9, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
take
BO
; for p, q being bag of n holds
( [p,q] in BO iff p <=' q )
let p, q be bag of n; ( [p,q] in BO iff p <=' q )
hereby ( p <=' q implies [p,q] in BO )
end;
( p in Bags n & q in Bags n )
by Def12;
hence
( p <=' q implies [p,q] in BO )
by A1; verum