:: deftheorem defines is_proper_subformula_of MODELC_2:def 23 :
for H, F being LTL-formula holds
( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );