let IT1, IT2 be bag of n; :: thesis: ( 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 ; :: thesis: IT1 = IT2
A36: IT1 <= IT2,T by A32, A35;
IT2 <= IT1,T by A33, A34;
hence IT1 = IT2 by A36, TERMORD:7; :: thesis: verum