for p being Element of LTLB_WFF holds p => p is ctaut