set C = { a where a is Element of A : a is Zero_Divisor of A } ;
for x being object st x in { a where a is Element of A : a is Zero_Divisor of A } holds
x in [#] A

proof

let x be object ; :: thesis: ( x in { a where a is Element of A : a is Zero_Divisor of A } implies x in [#] A )
assume x in { a where a is Element of A : a is Zero_Divisor of A } ; :: thesis: x in [#] A
then ex a being Element of [#] A st
( x = a & a is Zero_Divisor of A ) ;
hence x in [#] A ; :: thesis: verum

end;

then { a where a is Element of A : a is Zero_Divisor of A } c= [#] A ;
hence { a where a is Element of A : a is Zero_Divisor of A } is Subset of A ; :: thesis: verum