let C be ConstructorSignature; :: thesis: ( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) )

hereby :: thesis: ( ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) implies C is initialized )

assume C is initialized ; :: thesis: ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary )
then consider m, a being OperSymbol of C such that
A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) ;
reconsider m = m as OperSymbol of a_Type C by A1, ABCMIZ_1:def 32;
reconsider a = a as OperSymbol of an_Adj C by A1, ABCMIZ_1:def 32;
take m = m; :: thesis: ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary )
take a = a; :: thesis: ( m is nullary & a is nullary )
thus m is nullary by A1; :: thesis: a is nullary
thus a is nullary by A1; :: thesis: verum

end;

given m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that A2: ( m is nullary & a is nullary ) ; :: thesis: C is initialized
take m ; :: according to ABCMIZ_1:def 12 :: thesis: ex b₁ being Element of the carrier' of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b₁ = an_Adj & the_arity_of b₁ = {} )
take a ; :: thesis: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} )
( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38;
hence ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A2, ABCMIZ_1:def 32; :: thesis: verum