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