theorem Th25: :: LTLAXIO2:25

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