theorem :: LTLAXIO2:51

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