:: deftheorem defines |-0 LTLAXIO5:def 11 :
for X being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( X |-0 p iff ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) ) );