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