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