:: deftheorem defines untn LTLAXIO4:def 8 :
for X being Subset of LTLB_WFF holds untn X = { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;