theorem :: ABCMIZ_A:53

for C being initialized ConstructorSignature
for t1, t2 being expression of C
for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1 ;