for t being GRZ-formula holds
( t is being_equality iff ex u, v being GRZ-formula st t = u '=' v )