let X, Y be set ; :: thesis:
thus proj1 (X \/ Y) c= (proj1 X) \/ (proj1 Y) :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in proj1 (X \/ Y) ; :: thesis:
then consider y being set such that
A1: [x,y] in X \/ Y by RELAT_1:def 4;
( [x,y] in X or [x,y] in Y ) by A1, XBOOLE_0:def 3;
then ( x in proj1 X or x in proj1 Y ) by RELAT_1:def 4;
hence x in (proj1 X) \/ (proj1 Y) by XBOOLE_0:def 3; :: thesis:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in proj2 (X \/ Y) ; :: thesis:
then consider x being set such that
A6: [x,y] in X \/ Y by RELAT_1:def 5;
( [x,y] in X or [x,y] in Y ) by A6, XBOOLE_0:def 3;
then ( y in proj2 X or y in proj2 Y ) by RELAT_1:def 5;
hence y in (proj2 X) \/ (proj2 Y) by XBOOLE_0:def 3; :: thesis:

end;