proj2 D c= the carrier of L2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 D or y in the carrier of L2 )
assume y in proj2 D ; :: thesis: y in the carrier of L2
then A2: ex x being object st [x,y] in D by XTUPLE_0:def 13;
the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2;
hence y in the carrier of L2 by A2, ZFMISC_1:87; :: thesis: verum

end;

hence proj2 D is Subset of L2 ; :: thesis: verum