theorem :: LTLAXIO1:60

for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q))