let I be set ; :: thesis: for X, Y being ManySortedSet of I st Y is empty-yielding & X c= Y holds
X is empty-yielding
let X, Y be ManySortedSet of I; :: thesis: ( Y is empty-yielding & X c= Y implies X is empty-yielding )
assume A1: ( Y is empty-yielding & X c= Y ) ; :: thesis: X is empty-yielding
let i be object ; :: according to PBOOLE:def 12 :: thesis: ( i in I implies X . i is empty )
assume i in I ; :: thesis: X . i is empty
then ( X . i c= Y . i & Y . i is empty ) by A1;
hence X . i is empty ; :: thesis: verum