:: deftheorem defines -correct GRZLOG_1:def 30 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P being GRZ-formula-sequence holds
( P is A,R -correct iff for k being Element of NAT st k in dom P holds
P,k is_a_correct_step_wrt A,R );