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

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