let X, Y be set ; :: thesis:
( (proj1 X) \+\ (proj1 Y) = ((proj1 X) \ (proj1 Y)) \/ ((proj1 Y) \ (proj1 X)) & (proj2 X) \+\ (proj2 Y) = ((proj2 X) \ (proj2 Y)) \/ ((proj2 Y) \ (proj2 X)) & (proj1 X) \ (proj1 Y) c= proj1 (X \ Y) & (proj2 X) \ (proj2 Y) c= proj2 (X \ Y) & (proj1 Y) \ (proj1 X) c= proj1 (Y \ X) & (proj2 Y) \ (proj2 X) c= proj2 (Y \ X) & X \+\ Y = (X \ Y) \/ (Y \ X) ) by Th8;
then ( (proj1 X) \+\ (proj1 Y) c= (proj1 (X \ Y)) \/ (proj1 (Y \ X)) & (proj2 X) \+\ (proj2 Y) c= (proj2 (X \ Y)) \/ (proj2 (Y \ X)) & (proj1 (X \ Y)) \/ (proj1 (Y \ X)) = proj1 (X \+\ Y) & (proj2 (X \ Y)) \/ (proj2 (Y \ X)) = proj2 (X \+\ Y) ) by Th6, XBOOLE_1:13;
hence ( (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y) & (proj2 X) \+\ (proj2 Y) c= proj2 (X \+\ Y) ) ; :: thesis: