for G, H being LTL-formula holds
( G in Subformulae H iff G is_subformula_of H )