let p, q be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st p => q in F holds

F \/ {p} |- 'G' q

let F be Subset of LTLB_WFF; :: thesis: ( p => q in F implies F \/ {p} |- 'G' q )

p in {p} by TARSKI:def 1;

then p in F \/ {p} by XBOOLE_0:def 3;

then A1: F \/ {p} |- p by Th42;

assume p => q in F ; :: thesis: F \/ {p} |- 'G' q

then p => q in F \/ {p} by XBOOLE_0:def 3;

then F \/ {p} |- p => q by Th42;

then F \/ {p} |- q by A1, Th43;

hence F \/ {p} |- 'G' q by Th54; :: thesis: verum

F \/ {p} |- 'G' q

let F be Subset of LTLB_WFF; :: thesis: ( p => q in F implies F \/ {p} |- 'G' q )

p in {p} by TARSKI:def 1;

then p in F \/ {p} by XBOOLE_0:def 3;

then A1: F \/ {p} |- p by Th42;

assume p => q in F ; :: thesis: F \/ {p} |- 'G' q

then p => q in F \/ {p} by XBOOLE_0:def 3;

then F \/ {p} |- p => q by Th42;

then F \/ {p} |- q by A1, Th43;

hence F \/ {p} |- 'G' q by Th54; :: thesis: verum