:: deftheorem Def24 defines Subformulae MODELC_2:def 24 :
for H being LTL-formula
for b₂ being set holds
( b₂ = Subformulae H iff for a being set holds
( a in b₂ iff ex F being LTL-formula st
( F = a & F is_subformula_of H ) ) );