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 object ; :: 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 object ; :: 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