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 object ; :: 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 object st [x,y] in [:X,Y:] by XTUPLE_0:def 12;
hence x in X by ZFMISC_1:87; :: thesis: verum
end;
let y be object ; :: 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 object st [x,y] in [:X,Y:] by XTUPLE_0:def 13;
hence y in Y by ZFMISC_1:87; :: thesis: verum