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