theorem Th14: :: MODELC_2:14

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