theorem Th5: :: LTLAXIO5:32

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