theorem th21cp: :: LTLAXIO5:17

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