let t1, t2 be expression of C; :: thesis: ( ex f being valuation of C st f unifies t1,t2 implies ex f being valuation of C st f unifies t2,t1 )
given f being valuation of C such that A1: f unifies t1,t2 ; :: thesis: ex f being valuation of C st f unifies t2,t1
take f ; :: thesis: f unifies t2,t1
thus t2 at f = t1 at f by A1; :: according to ABCMIZ_A:def 24 :: thesis: verum