theorem th264p: :: LTLAXIO5:22

'G' ({} LTLB_WFF) = {} LTLB_WFF