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

(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; :: thesis: verum

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

(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; :: thesis: verum