let f be valuation of C; :: thesis: ( f is empty implies f is irrelevant )
assume f is empty ; :: thesis: f is irrelevant
then reconsider f = f as empty valuation of C ;
let x be variable; :: according to ABCMIZ_1:def 58 :: thesis: ( x in dom f implies ex y being variable st f . x = y -term C )
dom f = {} ;
hence ( x in dom f implies ex y being variable st f . x = y -term C ) ; :: thesis: verum