:: deftheorem defines |- PL_AXIOM:def 26 :
for F being Subset of PL-WFF
for p being Element of PL-WFF holds
( F |- p iff ex f being FinSequence of PL-WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) ) );