scheme :: ZF_LANG:sch 2
ZFCompInd{ P1[ ZF-formula] } :
for H being ZF-formula holds P1[H]
provided
A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds
P1[F] ) holds
P1[H]