theorem :: LTLAXIO2:37

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