:: deftheorem defines closed_wrt_A1-A7 ZF_FUND1:def 13 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A1-A7 iff ( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 ) );