:: deftheorem Def29 defines prc LTLAXIO1:def 29 :
for i being Nat
for f being FinSequence of LTLB_WFF
for X being Subset of LTLB_WFF holds
( prc f,X,i iff ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) );