:: deftheorem defines is_proper_subformula_of ZF_LANG:def 41 :
for H, F being ZF-formula holds
( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );