theorem Th24: :: LTLAXIO2:24

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