scheme :: ZF_LANG:sch 2
ZFCompInd{ P₁[ ZF-formula] } :

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

provided

A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds
P₁[F] ) holds
P₁[H]