theorem th19: :: LTLAXIO5:7

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