let X, Y be set ; :: thesis: (proj1_3 X) \+\ (proj1_3 Y) c= proj1_3 (X \+\ Y)
( (proj1_3 X) \ (proj1_3 Y) c= proj1_3 (X \ Y) & (proj1_3 Y) \ (proj1_3 X) c= proj1_3 (Y \ X) ) by Th33;
then (proj1_3 X) \+\ (proj1_3 Y) c= (proj1_3 (X \ Y)) \/ (proj1_3 (Y \ X)) by XBOOLE_1:13;
hence (proj1_3 X) \+\ (proj1_3 Y) c= proj1_3 (X \+\ Y) by Th31; :: thesis: verum