:: deftheorem Def1 defines rarg LTLAXIO4:def 1 :
for A being Element of LTLB_WFF st A is s-until holds
for b₂ being Element of LTLB_WFF holds
( b₂ = rarg A iff ex p being Element of LTLB_WFF st p 'U' b₂ = A );