:: deftheorem defines predicatively_closed ZF_FUND2:def 2 :
for M being non empty set holds
( M is predicatively_closed iff for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st E in M holds
Section (H,f) in M );