:: deftheorem Def1 defines Section ZF_FUND2:def 1 :
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( ( x. 0 in Free H implies Section (H,v) = { m where m is Element of M : M,v / ((x. 0),m) |= H } ) & ( not x. 0 in Free H implies Section (H,v) = {} ) );