let X, Y be set ; :: thesis: (proj2_4 X) \+\ (proj2_4 Y) c= proj2_4 (X \+\ Y)
( (proj2_4 X) \ (proj2_4 Y) c= proj2_4 (X \ Y) & (proj2_4 Y) \ (proj2_4 X) c= proj2_4 (Y \ X) ) by Th45;
then (proj2_4 X) \+\ (proj2_4 Y) c= (proj2_4 (X \ Y)) \/ (proj2_4 (Y \ X)) by XBOOLE_1:13;
hence (proj2_4 X) \+\ (proj2_4 Y) c= proj2_4 (X \+\ Y) by Th43; :: thesis: verum