set M9 = { (% d) where d is Element of (LattPOSet L) : d in D } ;
for x being object st x in { (% d) where d is Element of (LattPOSet L) : d in D } holds
x in the carrier of L

proof

let x be object ; :: thesis: ( x in { (% d) where d is Element of (LattPOSet L) : d in D } implies x in the carrier of L )
assume x in { (% d) where d is Element of (LattPOSet L) : d in D } ; :: thesis: x in the carrier of L
then ex x9 being Element of (LattPOSet L) st
( x = % x9 & x9 in D ) ;
hence x in the carrier of L ; :: thesis: verum

end;

hence { (% d) where d is Element of (LattPOSet L) : d in D } is Subset of L by TARSKI:def 3; :: thesis: verum