theorem :: LTLAXIO2:63

for A, B being Element of LTLB_WFF
for X being Subset of LTLB_WFF holds X |- ('not' (A 'U' B)) => ('X' ('not' (untn (A,B))))