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

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

end;