for x being object st x in judgefunc " {TRUE} holds
x in dom judgefunc by FUNCT_1:def 7;
hence judgefunc " {TRUE} is Event of (dom judgefunc) by TARSKI:def 3; :: thesis: verum