theorem Th31: :: LTLAXIO2:31

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