theorem Th4: :: LTLAXIO2:4

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