theorem Th13: :: ABCMIZ_A:13
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )