( * in {* ,non_op } & non_op in {* ,non_op } & the carrier' of MaxConstrSign = {* ,non_op } \/ Constructors ) by TARSKI:def 2, ABCMIZ_1:def 24;
then ( c <> * & c <> non_op & c in the carrier' of MaxConstrSign ) by XBOOLE_0:def 3, XBOOLE_0:3, ABCMIZ_1:39;
hence c is constructor OperSymbol of MaxConstrSign by ABCMIZ_1:def 11; :: thesis: verum