:: deftheorem defines 'R' LTLAXIO1:def 9 :
for p, q being Element of LTLB_WFF holds p 'R' q = 'not' (('not' p) 'Uw' ('not' q));