let p, q be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q))
let F be Subset of LTLB_WFF; :: thesis: F |- ('G' (p => q)) => (('G' p) => ('G' q))
reconsider G = (F \/ {(p => q)}) \/ {p} as Subset of LTLB_WFF ;
p => q in {(p => q)} by TARSKI:def 1;
then p => q in F \/ {(p => q)} by XBOOLE_0:def 3;
then G |- 'G' q by Th55;
then F \/ {(p => q)} |- ('G' p) => ('G' q) by Th57;
hence F |- ('G' (p => q)) => (('G' p) => ('G' q)) by Th57; :: thesis: verum