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