for F, H being LTL-formula holds
( H is_immediate_constituent_of 'X' F iff H = F )