:: deftheorem defines -correct PROOFS_1:def 7 :
for B being set
for R being Rule
for P being Formula-sequence holds
( P is B,R -correct iff for k being Nat st k in dom P holds
P,k is_a_correct_step_wrt B,R );