theorem Th23: :: LTLAXIO2:23

for p being Element of LTLB_WFF holds ('not' TVERUM) => p is ctaut