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 set ; :: 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, Def4;
then x . i in (X . i) /\ (Y . i) by A2, Def8;
hence x . i in X . i by XBOOLE_0:def 4; :: thesis: verum

end;

thus x in Y :: thesis: verum

proof

let i be set ; :: 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, Def4;
then x . i in (X . i) /\ (Y . i) by A3, Def8;
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 set ; :: 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, Def4;
then x . i in (X . i) /\ (Y . i) by XBOOLE_0:def 4;
hence x . i in (X /\ Y) . i by A5, Def8; :: thesis: verum