:: deftheorem defines being_equality GRZLOG_1:def 20 :
for t being GRZ-formula holds
( t is being_equality iff Polish-WFF-head t = '=' );