let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X c= X \/ Y
let X, Y be ManySortedSet of I; :: thesis: X c= X \/ Y
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies X . i c= (X \/ Y) . i )
assume A1: i in I ; :: thesis: X . i c= (X \/ Y) . i
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in X . i or e in (X \/ Y) . i )
assume e in X . i ; :: thesis: e in (X \/ Y) . i
then e in (X . i) \/ (Y . i) by XBOOLE_0:def 3;
hence e in (X \/ Y) . i by A1, Def4; :: thesis: verum