theorem :: MODELC_2:19

for F, H being LTL-formula st F is atomic holds
not H is_immediate_constituent_of F