:: deftheorem defprc defines prc PL_AXIOM:def 25 :
for i being Nat
for f being FinSequence of PL-WFF
for F being Subset of PL-WFF holds
( prc f,F,i iff ( f . i in PL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) );