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