:: deftheorem defines is_immediate_constituent_of ZF_LANG:def 39 :
for H, F being ZF-formula holds
( H is_immediate_constituent_of F iff ( F = 'not' H or ex H1 being ZF-formula st
( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ) );