let A, B be Element of LTLB_WFF ; for F being Subset of LTLB_WFF st F |= A & F |= A => B holds
F |= B
let F be Subset of LTLB_WFF; ( F |= A & F |= A => B implies F |= B )
assume that
A1:
F |= A
and
A2:
F |= A => B
; F |= B
let M be LTLModel; LTLAXIO1:def 14 ( M |= F implies M |= B )
assume A3:
M |= F
; M |= B
let n be Element of NAT ; LTLAXIO1:def 12 (SAT M) . [n,B] = 1
(SAT M) . [n,(A => B)] = 1
by Def12, A2, A3;
then A4:
((SAT M) . [n,A]) => ((SAT M) . [n,B]) = 1
by Def11;
(SAT M) . [n,A] = 1
by Def12, A1, A3;
hence
(SAT M) . [n,B] = 1
by A4; verum