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

F |=0 B

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

assume that

A1: F |=0 A and

A2: F |=0 A => B ; :: thesis: F |=0 B

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 B )

assume B3: M |=0 F ; :: thesis: M |=0 B

then M |=0 A => B by A2;

then B6: ((SAT M) . [0,A]) => ((SAT M) . [0,B]) = 1 by LTLAXIO1:def 11;

M |=0 A by A1, B3;

hence M |=0 B by B6; :: thesis: verum

F |=0 B

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

assume that

A1: F |=0 A and

A2: F |=0 A => B ; :: thesis: F |=0 B

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 B )

assume B3: M |=0 F ; :: thesis: M |=0 B

then M |=0 A => B by A2;

then B6: ((SAT M) . [0,A]) => ((SAT M) . [0,B]) = 1 by LTLAXIO1:def 11;

M |=0 A by A1, B3;

hence M |=0 B by B6; :: thesis: verum