set M' = { (d % ) where d is Element of L : d in D } ;
for x being set 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 set ; :: 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 x' being Element of L st
( x = x' % & x' 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