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