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 C idval (variables_in t) ; :: thesis: ( variables_in t c= dom (C idval (variables_in t)) & t,t at (C idval (variables_in t)) are_unifiable )
thus ( variables_in t c= dom (C idval (variables_in t)) & t,t at (C idval (variables_in t)) are_unifiable ) by ABCMIZ_1:131, ABCMIZ_1:137; :: thesis: verum