let I be set ; :: thesis: for X, A being ManySortedSet of I st X in A holds
X c= union A
let X, A be ManySortedSet of I; :: thesis: ( X in A implies X c= union A )
assume A1: X in A ; :: thesis: X c= union A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or X . i c= (union A) . i )
assume A2: i in I ; :: thesis: X . i c= (union A) . i
then X . i in A . i by A1, PBOOLE:def 4;
then X . i c= union (A . i) by ZFMISC_1:92;
hence X . i c= (union A) . i by A2, Def2; :: thesis: verum