let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
let n be Element of NAT ; :: thesis: for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
let M be LTLModel; :: thesis: ( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )

hereby :: thesis: ( ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 implies (SAT M) . [n,('F' A)] = 1 )

assume (SAT M) . [n,('F' A)] = 1 ; :: thesis: ex i being Element of NAT st (SAT M) . [(n + i),A] = 1
then (SAT M) . [n,('G' ('not' A))] = 0 by Th6;
then consider i being Element of NAT such that
A1: not (SAT M) . [(n + i),('not' A)] = 1 by Th11;
not (SAT M) . [(n + i),A] = 0 by A1, Th6;
then (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def 3;
hence ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 ; :: thesis: verum

end;

assume ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 ; :: thesis: (SAT M) . [n,('F' A)] = 1
then consider i being Element of NAT such that
A2: (SAT M) . [(n + i),A] = 1 ;
not (SAT M) . [(n + i),('not' A)] = 1 by A2, Th6;
then not (SAT M) . [n,('G' ('not' A))] = 1 by Th11;
then (SAT M) . [n,('G' ('not' A))] = 0 by XBOOLEAN:def 3;
hence (SAT M) . [n,('F' A)] = 1 by Th6; :: thesis: verum