let p be Element of LTLB_WFF ; :: thesis: p is FinSequence of NAT
LTLB_WFF c= NAT * by HILBERT1:def 5;
then p in NAT * ;
hence p is FinSequence of NAT by FINSEQ_1:def 11; :: thesis: verum