:: deftheorem defines trueEVENT DIST_2:def 3 :
for judgefunc being BOOLEAN -valued Function holds trueEVENT judgefunc = judgefunc " {TRUE};