for p, q being Element of LTLB_WFF st p in tau1 . q & p <> q holds
len p < len q