:: deftheorem Def3 defines GRZ-op-arity GRZLOG_1:def 7 :
for b₁ being Function of GRZ-ops,NAT holds
( b₁ = GRZ-op-arity iff ( b₁ . 'not' = 1 & b₁ . '&' = 2 & b₁ . '=' = 2 ) );