let i be Element of NAT ; :: thesis: ( {(prop i)} |- prop i & not {(prop i)} |-0 'G' (prop i) )
prop i in {(prop i)} by TARSKI:def 1;
hence {(prop i)} |- prop i by LTLAXIO1:42; :: thesis: not {(prop i)} |-0 'G' (prop i)
thus not {(prop i)} |-0 'G' (prop i) by th266, th21cp; :: thesis: verum