theorem :: LTLAXIO5:52

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