let I be set ; :: thesis: for X, Y being ManySortedSet of I st X is V8() & X c= Y holds
Y is V8()
let X, Y be ManySortedSet of I; :: thesis: ( X is V8() & X c= Y implies Y is V8() )
assume A1: ( X is V8() & X c= Y ) ; :: thesis: Y is V8()
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