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