let I be set ; :: thesis: for X, Y being ManySortedSet of I holds
( X /\ Y c= X & X /\ Y c= Y )
let X, Y be ManySortedSet of I; :: thesis: ( X /\ Y c= X & X /\ Y c= Y )
thus X /\ Y c= X :: thesis: X /\ Y c= Y

proof

let i be set ; :: 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 set ; :: 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, Def8;
hence e in X . i by XBOOLE_0:def 4; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies (X /\ Y) . i c= Y . i )
assume A2: i in I ; :: thesis: (X /\ Y) . i c= Y . i
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in (X /\ Y) . i or e in Y . i )
assume e in (X /\ Y) . i ; :: thesis: e in Y . i
then e in (X . i) /\ (Y . i) by A2, Def8;
hence e in Y . i by XBOOLE_0:def 4; :: thesis: verum