{ a where a is Element of L : a * = Bottom L } c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of L : a * = Bottom L } or x in the carrier of L )
assume x in { a where a is Element of L : a * = Bottom L } ; :: thesis: x in the carrier of L
then consider aa being Element of L such that
A1: ( aa = x & aa * = Bottom L ) ;
thus x in the carrier of L by A1; :: thesis: verum

end;

hence { a where a is Element of L : a * = Bottom L } is Subset of L ; :: thesis: verum