proj1 D c= the carrier of L1

proof

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

end;

hence proj1 D is Subset of L1 ; :: thesis: verum