theorem :: LTLAXIO5:54

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