for H being LTL-formula holds H is_subformula_of H ;