theorem :: LTLAXIO2:42

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