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