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