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