theorem :: MODELC_2:46

for F, H being LTL-formula st F is_subformula_of H holds
Subformulae F c= Subformulae H