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