theorem Th46: :: ABCMIZ_1:46
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds
( (ast C) term (a,t) is expression of C, a_Type C & (ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> )