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

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