theorem Th2: :: LTLAXIO4:2

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