:: deftheorem Def29 defines prc0 LTLAXIO5:def 10 :
for i being Nat
for f being FinSequence of LTLB_WFF
for X being Subset of LTLB_WFF holds
( prc0 f,X,i iff ( f . i in LTL0_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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) );