:: deftheorem defines is_a_correct_step_wrt PROOFS_1:def 6 :
for B being set
for R being Rule
for P being Formula-sequence
for n being Nat holds
( P,n is_a_correct_step_wrt B,R iff ( P . n in B or ex Q being Formula-finset st
( [Q,(P . n)] in R & ( for t being object st t in Q holds
ex k being Nat st
( k in dom P & k < n & P . k = t ) ) ) ) );