for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st untn (p,q) in tau X holds
( p in tau X & q in tau X & p 'U' q in tau X )