let B1, B2 be Order of (Bags n); ( ( for p, q being bag of n holds
( [p,q] in B1 iff p <=' q ) ) & ( for p, q being bag of n holds
( [p,q] in B2 iff p <=' q ) ) implies B1 = B2 )
assume that
A17:
for p, q being bag of n holds
( [p,q] in B1 iff p <=' q )
and
A18:
for p, q being bag of n holds
( [p,q] in B2 iff p <=' q )
; B1 = B2
let a, b be object ; RELAT_1:def 2 ( ( not [a,b] in B1 or [a,b] in B2 ) & ( not [a,b] in B2 or [a,b] in B1 ) )
hereby ( not [a,b] in B2 or [a,b] in B1 )
assume A19:
[a,b] in B1
;
[a,b] in B2then consider b1,
b2 being
object such that A20:
[a,b] = [b1,b2]
and A21:
(
b1 in Bags n &
b2 in Bags n )
by RELSET_1:2;
reconsider b1 =
b1,
b2 =
b2 as
bag of
n by A21;
b1 <=' b2
by A17, A19, A20;
hence
[a,b] in B2
by A18, A20;
verum
end;
assume A22:
[a,b] in B2
; [a,b] in B1
then consider b1, b2 being object such that
A23:
[a,b] = [b1,b2]
and
A24:
( b1 in Bags n & b2 in Bags n )
by RELSET_1:2;
reconsider b1 = b1, b2 = b2 as bag of n by A24;
b1 <=' b2
by A18, A22, A23;
hence
[a,b] in B1
by A17, A23; verum