let C be initialized ConstructorSignature; :: thesis: for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds
A1 matches_with A3
let t1, t2, t3 be Subset of (QuasiAdjs C); :: thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 )
given f1 being valuation of C such that A1: t2 at f1 c= t1 ; :: according to ABCMIZ_A:def 22 :: thesis: ( not t2 matches_with t3 or t1 matches_with t3 )
given f2 being valuation of C such that A2: t3 at f2 c= t2 ; :: according to ABCMIZ_A:def 22 :: thesis: t1 matches_with t3
take f2 at f1 ; :: according to ABCMIZ_A:def 22 :: thesis: t3 at (f2 at f1) c= t1
(t3 at f2) at f1 c= t2 at f1 by A2, ABCMIZ_1:146;
then (t3 at f2) at f1 c= t1 by A1;
hence t3 at (f2 at f1) c= t1 by ABCMIZ_1:150; :: thesis: verum