let p, q be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |- ('G' p) => q holds
F \/ {p} |- q
let F be Subset of LTLB_WFF; :: thesis: ( F |- ('G' p) => q implies F \/ {p} |- q )
p in {p} by TARSKI:def 1;
then p in F \/ {p} by XBOOLE_0:def 3;
then F \/ {p} |- p by Th42;
then A1: F \/ {p} |- 'G' p by Th54;
assume F |- ('G' p) => q ; :: thesis: F \/ {p} |- q
then F \/ {p} |- ('G' p) => q by Th56;
hence F \/ {p} |- q by A1, Th43; :: thesis: verum