for F, G, H being LTL-formula holds
( not F is_proper_subformula_of G 'or' H or F is_subformula_of G or F is_subformula_of H )