the_result_sort_of (ast C) = a_Type C by Def9;
hence ex o being OperSymbol of C st the_result_sort_of o = a_Type C ; :: according to ABCMIZ_1:def 32 :: thesis: the_result_sort_of (ast C) = a_Type C
thus the_result_sort_of (ast C) = a_Type C by Def9; :: thesis: verum