let I be set ; :: thesis: for X, Y being ManySortedSet of st X is non-empty & X [= Y holds
Y is non-empty
let X, Y be ManySortedSet of ; :: thesis: ( X is non-empty & X [= Y implies Y is non-empty )
assume A1: X is non-empty ; :: thesis: ( not X [= Y or Y is non-empty )
assume X [= Y ; :: thesis: Y is non-empty
then X c= Y by A1, Th144;
hence Y is non-empty by A1, Th143; :: thesis: verum