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