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