A1: m `1 in {a_Type} by MCART_1:10;
the_result_sort_of (@ m) = m `1 by ABCMIZ_1:def 24
.= a_Type by A1, TARSKI:def 1 ;
hence @ m is constructor OperSymbol of a_Type MaxConstrSign by ABCMIZ_1:def 32; :: thesis: verum