:: deftheorem defines closed_wrt_A3 ZF_FUND1:def 8 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A3 iff for a being Element of V st a in X holds
union a in X );