theorem :: ABCMIZ_A:15

for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Constructors holds
e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)