theorem th14: :: LTLAXIO5:45

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