let A be Element of LTLB_WFF ; :: thesis: {A} |= 'G' ('X' A)
assume not {A} |= 'G' ('X' A) ; :: thesis: contradiction
then consider M being LTLModel such that
A1: ( M |= {A} & not M |= 'G' ('X' A) ) ;
consider i being Element of NAT such that
A2: not (SAT M) . [i,('G' ('X' A))] = 1 by A1;
consider j being Element of NAT such that
A3: not (SAT M) . [(i + j),('X' A)] = 1 by A2, LTLAXIO1:10;
A4: not (SAT M) . [((i + j) + 1),A] = 1 by A3, LTLAXIO1:9;
A in {A} by TARSKI:def 1;
then M |= A by A1;
hence contradiction by A4; :: thesis: verum