theorem Th45: :: LTLAXIO1:45

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