let X, Y be set ; :: thesis: ( proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y) & proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y) )
thus proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y) :: thesis: proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 (X /\ Y) or x in (proj1 X) /\ (proj1 Y) )
assume x in proj1 (X /\ Y) ; :: thesis: x in (proj1 X) /\ (proj1 Y)
then consider y being set such that
A1: [x,y] in X /\ Y by RELAT_1:def 4;
[x,y] in Y by A1, XBOOLE_0:def 4;
then A2: x in proj1 Y by RELAT_1:def 4;
[x,y] in X by A1, XBOOLE_0:def 4;
then x in proj1 X by RELAT_1:def 4;
hence x in (proj1 X) /\ (proj1 Y) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 (X /\ Y) or y in (proj2 X) /\ (proj2 Y) )
assume y in proj2 (X /\ Y) ; :: thesis: y in (proj2 X) /\ (proj2 Y)
then consider x being set such that
A3: [x,y] in X /\ Y by RELAT_1:def 5;
[x,y] in Y by A3, XBOOLE_0:def 4;
then A4: y in proj2 Y by RELAT_1:def 5;
[x,y] in X by A3, XBOOLE_0:def 4;
then y in proj2 X by RELAT_1:def 5;
hence y in (proj2 X) /\ (proj2 Y) by A4, XBOOLE_0:def 4; :: thesis: verum