theorem :: ABCMIZ_1:56

for C being initialized ConstructorSignature
for a, b being expression of C, an_Adj C
for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term (b,t)