let I be set ; :: thesis: for x, X, Y being ManySortedSet of I holds
( x in X (/\) Y iff ( x in X & x in Y ) )
let x, X, Y be ManySortedSet of I; :: thesis: ( x in X (/\) Y iff ( x in X & x in Y ) )

hereby :: thesis: ( x in X & x in Y implies x in X (/\) Y )

assume A1: x in X (/\) Y ; :: thesis: ( x in X & x in Y )
thus x in X :: thesis: x in Y

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies x . i in X . i )
assume A2: i in I ; :: thesis: x . i in X . i
then x . i in (X (/\) Y) . i by A1;
then x . i in (X . i) /\ (Y . i) by A2, Def5;
hence x . i in X . i by XBOOLE_0:def 4; :: thesis: verum

end;

thus x in Y :: thesis: verum

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies x . i in Y . i )
assume A3: i in I ; :: thesis: x . i in Y . i
then x . i in (X (/\) Y) . i by A1;
then x . i in (X . i) /\ (Y . i) by A3, Def5;
hence x . i in Y . i by XBOOLE_0:def 4; :: thesis: verum

end;

end;

assume A4: ( x in X & x in Y ) ; :: thesis: x in X (/\) Y
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies x . i in (X (/\) Y) . i )
assume A5: i in I ; :: thesis: x . i in (X (/\) Y) . i
then ( x . i in X . i & x . i in Y . i ) by A4;
then x . i in (X . i) /\ (Y . i) by XBOOLE_0:def 4;
hence x . i in (X (/\) Y) . i by A5, Def5; :: thesis: verum