let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y holds
X \/ Y = Y
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y implies X \/ Y = Y )
assume X c= Y ; :: thesis: X \/ Y = Y
then A1: X \/ Y c= Y by Th16;
Y c= X \/ Y by Th14;
hence X \/ Y = Y by A1, Lm1; :: thesis: verum