theorem th13: :: LTLAXIO5:41

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' (A => B) & F |-0 'G' (A => ('X' A)) holds
F |-0 'G' (A => ('G' B))