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