:: deftheorem defines -diagFormula FOMODEL4:def 76 :
for S being Language holds S -diagFormula = { [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } ;