theorem Th8: :: MODELC_2:8

for H being LTL-formula st H is Until holds
H = (the_left_argument_of H) 'U' (the_right_argument_of H)