theorem :: ABCMIZ_A:51
for C being initialized ConstructorSignature
for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds
A1 matches_with A3