theorem Th43: :: LTLAXIO2:43

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