theorem Th26: :: LTLAXIO2:26

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