theorem :: MODELC_3:71

for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula st w |= 'X' v holds
w |= * (init v)