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

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