for p being Element of LTLB_WFF holds p is FinSequence of NAT