:: deftheorem defines |- GRZLOG_1:def 33 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for B being Subset of GRZ-formula-set holds
( A,R |- B iff for t being GRZ-formula st t in B holds
A,R |- t );