theorem :: LTLAXIO2:38

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