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