let IT1, IT2 be bag of n; ( IT1 in B & ( for x being bag of n st x in B holds
x <= IT1,T ) & IT2 in B & ( for x being bag of n st x in B holds
x <= IT2,T ) implies IT1 = IT2 )
assume that
A32:
IT1 in B
and
A33:
for x being bag of n st x in B holds
x <= IT1,T
and
A34:
IT2 in B
and
A35:
for x being bag of n st x in B holds
x <= IT2,T
; IT1 = IT2
A36:
IT1 <= IT2,T
by A32, A35;
IT2 <= IT1,T
by A33, A34;
hence
IT1 = IT2
by A36, TERMORD:7; verum