:: deftheorem defines GRZ-MP GRZLOG_1:def 24 :
GRZ-MP = { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;