theorem Th22: :: LTLAXIO2:22

for p being Element of LTLB_WFF holds p => TVERUM is ctaut