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 object ; :: according to TARSKI:def 3 :: thesis:
assume x in proj1 (X \/ Y) ; :: thesis:
then consider y being object such that
A1: [x,y] in X \/ Y by Def12;
( [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 Def12;
hence x in (proj1 X) \/ (proj1 Y) by XBOOLE_0:def 3; :: thesis:

end;