set I = { x where x is Element of L : a "/\" x = Bottom L } ;
{ x where x is Element of L : a "/\" x = Bottom L } c= the carrier of L

proof

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

end;

hence { x where x is Element of L : a "/\" x = Bottom L } is Subset of L ; :: thesis: verum