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 nin {*,non_op} ) by TARSKI:def 2;
hence ( o is constructor iff o in Constructors ) by A1, ABCMIZ_1:39, XBOOLE_0:3, XBOOLE_0:def 3; :: thesis: verum