set M = { a where a is nilpotent Element of A : verum } ;
{ a where a is nilpotent Element of A : verum } c= the carrier of A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is nilpotent Element of A : verum } or x in the carrier of A )
assume x in { a where a is nilpotent Element of A : verum } ; :: thesis: x in the carrier of A
then ex a being nilpotent Element of A st a = x ;
hence x in the carrier of A ; :: thesis: verum

end;

hence { a where a is nilpotent Element of A : verum } is Subset of A ; :: thesis: verum