let t be expression of C; :: thesis: ex g being one-to-one irrelevant valuation of C st
( variables_in t c= dom g & t,t at g are_unifiable )
take g = C idval (variables_in t); :: thesis: ( variables_in t c= dom g & t,t at g are_unifiable )
thus ( variables_in t c= dom g & t,t at g are_unifiable ) by ABCMIZ_1:137, ABCMIZ_1:131; :: thesis: verum