theorem th19a: :: LTLAXIO5:6

for A being Element of LTLB_WFF holds {A} |= 'G' ('X' A)