:: deftheorem Def35 defines GRZ-rules GRZLOG_1:def 28 :
for b₁ being GRZ-rule holds
( b₁ = GRZ-rules iff for a being object holds
( a in b₁ iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) );