scheme :: ZF_LANG:sch 1
ZFInd{ P1[ ZF-formula] } :
for H being ZF-formula holds P1[H]
provided
A1: for H being ZF-formula st H is atomic holds
P1[H] and
A2: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds
P1[H] and
A3: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds
P1[H] and
A4: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds
P1[H]