:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :
for C being initialized ConstructorSignature
for s being SortSymbol of C
for b₃ being expression of C holds
( b₃ is expression of C,s iff b₃ in the Sorts of (Free (C,(MSVars C))) . s );