let t be expression of C; :: thesis: ex f being valuation of C st t = t at f
take f = the empty valuation of C; :: thesis: t = t at f
thus t at f = t by ABCMIZ_1:139; :: thesis: verum