:: deftheorem defines |- LTLAXIO1:def 30 :
for X being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( X |- 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
prc f,X,i ) ) );