let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |=0 A holds

F |= A

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 A implies F |= A )

assume Z1: F |=0 A ; :: thesis: F |= A

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= F or M |= A )

assume A1: M |= F ; :: thesis: M |= A

let i be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [i,A] = 1

M ^\ i |=0 F by A1, LTLAXIO1:29, Th1;

then M ^\ i |=0 A by Z1;

then (SAT M) . [(i + 0),A] = 1 by LTLAXIO1:28;

hence (SAT M) . [i,A] = 1 ; :: thesis: verum

F |= A

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 A implies F |= A )

assume Z1: F |=0 A ; :: thesis: F |= A

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= F or M |= A )

assume A1: M |= F ; :: thesis: M |= A

let i be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [i,A] = 1

M ^\ i |=0 F by A1, LTLAXIO1:29, Th1;

then M ^\ i |=0 A by Z1;

then (SAT M) . [(i + 0),A] = 1 by LTLAXIO1:28;

hence (SAT M) . [i,A] = 1 ; :: thesis: verum