for F, G, H being LTL-formula holds
( H is_immediate_constituent_of F '&' G iff ( H = F or H = G ) )