theorem Th32: :: LTLAXIO2:32

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