theorem :: MODELC_2:76

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