let IT1, IT2 be bag of ; :: thesis: ( IT1 in B & ( for x being bag of st x in B holds
x <= IT1,T ) & IT2 in B & ( for x being bag of st x in B holds
x <= IT2,T ) implies IT1 = IT2 )
assume that
A23: IT1 in B and
A24: for x being bag of st x in B holds
x <= IT1,T and
A25: IT2 in B and
A26: for x being bag of st x in B holds
x <= IT2,T ; :: thesis: IT1 = IT2
A27: IT2 <= IT1,T by A24, A25;
IT1 <= IT2,T by A23, A26;
hence IT1 = IT2 by A27, TERMORD:7; :: thesis: verum