for g being Function of LTLB_WFF,BOOLEAN holds (VAL g) . TVERUM = 1