let C be Signature; :: thesis: ( C is constructor implies ( not C is empty & not C is void ) )
assume the carrier of C = {a_Type,an_Adj,a_Term} ; :: according to ABCMIZ_1:def 9 :: thesis: ( not {*,non_op} c= the carrier' of C or not the Arity of C . * = <*an_Adj,a_Type*> or not the Arity of C . non_op = <*an_Adj*> or not the ResultSort of C . * = a_Type or not the ResultSort of C . non_op = an_Adj or ex o being Element of the carrier' of C st
( o <> * & o <> non_op & not the Arity of C . o in {a_Term} * ) or ( not C is empty & not C is void ) )
assume {*,non_op} c= the carrier' of C ; :: thesis: ( not the Arity of C . * = <*an_Adj,a_Type*> or not the Arity of C . non_op = <*an_Adj*> or not the ResultSort of C . * = a_Type or not the ResultSort of C . non_op = an_Adj or ex o being Element of the carrier' of C st
( o <> * & o <> non_op & not the Arity of C . o in {a_Term} * ) or ( not C is empty & not C is void ) )
thus ( not the Arity of C . * = <*an_Adj,a_Type*> or not the Arity of C . non_op = <*an_Adj*> or not the ResultSort of C . * = a_Type or not the ResultSort of C . non_op = an_Adj or ex o being Element of the carrier' of C st
( o <> * & o <> non_op & not the Arity of C . o in {a_Term} * ) or ( not C is empty & not C is void ) ) ; :: thesis: verum