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 A2: M |= F ; :: thesis: M |= 'X' A
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 Th9
.= 1 by A2, Def12, A1 ; :: thesis: verum