let X, Y be set ; :: thesis: proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y)
let y be object ; :: 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 object such that
A1: [x,y] in X /\ Y by Def13;
[x,y] in Y by A1, XBOOLE_0:def 4;
then A2: y in proj2 Y by Def13;
[x,y] in X by A1, XBOOLE_0:def 4;
then y in proj2 X by Def13;
hence y in (proj2 X) /\ (proj2 Y) by A2, XBOOLE_0:def 4; :: thesis: verum