let I be set ; :: thesis: for A, X, Y being ManySortedSet of I st union Y c= A & X in Y holds
X c= A
let A, X, Y be ManySortedSet of I; :: thesis: ( union Y c= A & X in Y implies X c= A )
assume that
A1: union Y c= A and
A2: X in Y ; :: thesis: X c= A
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= A . i )
assume A3: i in I ; :: thesis: X . i c= A . i
then (union Y) . i c= A . i by A1;
then A4: union (Y . i) c= A . i by A3, Def2;
X . i in Y . i by A2, A3;
hence X . i c= A . i by A4, SETFAM_1:41; :: thesis: verum