theorem th262ac1: :: LTLAXIO5:14

for n being Element of NAT holds
( {(prop n)} |= 'X' (prop n) & not {(prop n)} |=0 'X' (prop n) )