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