theorem :: LTLAXIO2:39

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