let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds

( F \/ {A} |=0 B iff F |=0 A => B )

let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |=0 B iff F |=0 A => B )

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

assume M |=0 F \/ {A} ; :: thesis: M |=0 B

then A5: ( M |=0 F & M |=0 {A} ) by th263pa;

then A7: M |=0 A by th263pb;

M |=0 A => B by A5, A6;

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

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

( F \/ {A} |=0 B iff F |=0 A => B )

let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |=0 B iff F |=0 A => B )

hereby :: thesis: ( F |=0 A => B implies F \/ {A} |=0 B )

assume A6:
F |=0 A => B
; :: thesis: F \/ {A} |=0 Bassume A3:
F \/ {A} |=0 B
; :: thesis: F |=0 A => B

thus F |=0 A => B :: thesis: verum

end;thus F |=0 A => B :: thesis: verum

proof

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

assume A4: M |=0 F ; :: thesis: M |=0 A => B

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

thus M |=0 A => B :: thesis: verum

end;assume A4: M |=0 F ; :: thesis: M |=0 A => B

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

thus M |=0 A => B :: thesis: verum

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

assume M |=0 F \/ {A} ; :: thesis: M |=0 B

then A5: ( M |=0 F & M |=0 {A} ) by th263pa;

then A7: M |=0 A by th263pb;

M |=0 A => B by A5, A6;

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

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