{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } c= the carrier of L

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } or q in the carrier of L )
assume q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; :: thesis: q in the carrier of L
then consider a, b being Element of L such that
A1: ( q = a "/\" b & a in D1 & b in D2 ) ;
thus q in the carrier of L by A1; :: thesis: verum

end;

hence { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L ; :: thesis: verum