let X, Y be set ; :: thesis: proj2_4 (X /\ Y) c= (proj2_4 X) /\ (proj2_4 Y)
( proj2_4 (X /\ Y) c= proj2_4 X & proj2_4 (X /\ Y) c= proj2_4 Y ) by Th17, XBOOLE_1:17;
hence proj2_4 (X /\ Y) c= (proj2_4 X) /\ (proj2_4 Y) by XBOOLE_1:19; :: thesis: verum