:: deftheorem Def10 defines GRZ-axioms GRZLOG_1:def 21 :
for b₁ being non empty Subset of GRZ-formula-set holds
( b₁ = GRZ-axioms iff for a being object holds
( a in b₁ iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) ) );