:: deftheorem defines |- PROOFS_1:def 10 :
for B being set
for a being object
for R being Rule holds
( B,R |- a iff ex P being Formula-sequence st
( a in rng P & P is B,R -correct ) );