theorem Th75: :: MODELC_2:75

for H1, H2 being LTL-formula
for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'U' H2 iff r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) )