:: deftheorem defines matches_with ABCMIZ_A:def 23 :
for C being initialized ConstructorSignature
for T, P being quasi-type of C holds
( T matches_with P iff ex f being valuation of C st
( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T ) );