theorem :: MODELC_2:27

for H being LTL-formula holds H is_subformula_of H ;