theorem Th24: :: MODELC_2:24

for F, H being LTL-formula st F is Until holds
( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )