theorem th20: :: LTLAXIO5:8

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