scheme :: ZF_LANG:sch 1
ZFInd{ P₁[ ZF-formula] } :

for H being ZF-formula holds P₁[H]

provided

A1: for H being ZF-formula st H is atomic holds
P₁[H] and
A2: for H being ZF-formula st H is negative & P₁[ the_argument_of H] holds
P₁[H] and
A3: for H being ZF-formula st H is conjunctive & P₁[ the_left_argument_of H] & P₁[ the_right_argument_of H] holds
P₁[H] and
A4: for H being ZF-formula st H is universal & P₁[ the_scope_of H] holds
P₁[H]