theorem :: LTLAXIO2:41

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