:: deftheorem defines is_subformula_of ZF_LANG:def 40 :
for H, F being ZF-formula holds
( H is_subformula_of F iff ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );