:: deftheorem defines -correct GRZLOG_1:def 31 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for S being GRZ-formula-finset holds
( S is A,R -correct iff ex P being GRZ-formula-sequence st
( S = rng P & P is A,R -correct ) );