let I be set ; :: thesis: for Y, X being ManySortedSet of st Y is empty-yielding & X c= Y holds
X is empty-yielding
let Y, X be ManySortedSet of ; :: thesis: ( Y is empty-yielding & X c= Y implies X is empty-yielding )
assume that
A1: Y is empty-yielding and
A2: X c= Y ; :: thesis: X is empty-yielding
let i be set ; :: according to PBOOLE:def 15 :: thesis: ( i in I implies X . i is empty )
assume A3: i in I ; :: thesis: X . i is empty
then A4: X . i c= Y . i by A2, Def5;
Y . i is empty by A1, A3, Def15;
hence X . i is empty by A4, XBOOLE_1:3; :: thesis: verum