theorem :: ABCMIZ_A:26

for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )