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

proof

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

end;

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