theorem :: LTLAXIO2:50

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