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