let I be set ; :: thesis: for Y, X being ManySortedSet of I st Y is empty-yielding & X c= Y holds
X is empty-yielding
let Y, X 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 set ; :: 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, Def5, Def15;
hence X . i is empty by XBOOLE_1:3; :: thesis: verum