let X, Y be set ; :: thesis: ( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y )
thus proj1 [:X,Y:] c= X :: thesis: proj2 [:X,Y:] c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 [:X,Y:] or x in X )
assume x in proj1 [:X,Y:] ; :: thesis: x in X
then ex y being set st [x,y] in [:X,Y:] by RELAT_1:def 4;
hence x in X by ZFMISC_1:106; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 [:X,Y:] or y in Y )
assume y in proj2 [:X,Y:] ; :: thesis: y in Y
then ex x being set st [x,y] in [:X,Y:] by RELAT_1:def 5;
hence y in Y by ZFMISC_1:106; :: thesis: verum