:: deftheorem defines matches_with ABCMIZ_A:def 22 :
for C being initialized ConstructorSignature
for A, B being Subset of (QuasiAdjs C) holds
( A matches_with B iff ex f being valuation of C st B at f c= A );