theorem :: ABCMIZ_A:50

for C being initialized ConstructorSignature
for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds
t1 matches_with t3