let C be ConstructorSignature; :: thesis: ( C is standardized implies for o being OperSymbol of C holds
( o is constructor iff o in Constructors ) )
assume A1: C is standardized ; :: thesis: for o being OperSymbol of C holds
( o is constructor iff o in Constructors )
let o be OperSymbol of C; :: thesis: ( o is constructor iff o in Constructors )
thus ( o is constructor implies o in Constructors ) by A1; :: thesis: ( o in Constructors implies o is constructor )
assume o in Constructors ; :: thesis: o is constructor
then not o in {*,non_op} by ABCMIZ_1:39, XBOOLE_0:3;
hence ( o <> * & o <> non_op ) by TARSKI:def 2; :: according to ABCMIZ_1:def 11 :: thesis: verum