theorem Th45: :: MODELC_2:45

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