theorem Th16: :: MODELC_2:16

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