set X = { a where a is Element of L : a is completely-meet-irreducible } ;
for x being object st x in { a where a is Element of L : a is completely-meet-irreducible } holds
x in the carrier of L

proof

let x be object ; :: thesis: ( x in { a where a is Element of L : a is completely-meet-irreducible } implies x in the carrier of L )
assume x in { a where a is Element of L : a is completely-meet-irreducible } ; :: thesis: x in the carrier of L
then ex x9 being Element of L st
( x9 = x & x9 is completely-meet-irreducible ) ;
hence x in the carrier of L ; :: thesis: verum

end;

hence { a where a is Element of L : a is completely-meet-irreducible } is Subset of L by TARSKI:def 3; :: thesis: verum