for p, q, r being Element of LTLB_WFF st p => q in tau1 . r holds
( p in tau1 . r & q in tau1 . r )