let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |= A holds
F |= 'X' A
let F be Subset of LTLB_WFF; :: thesis: ( F |= A implies F |= 'X' A )
assume A1: F |= A ; :: thesis: F |= 'X' A
let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= 'X' A )
assume M |= F ; :: thesis: M |= 'X' A
then A2: M |= A by A1, Def15;
let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [n,('X' A)] = 1
thus (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] by Th10
.= 1 by A2, Def13 ; :: thesis: verum