take MaxConstrSign ; :: thesis: ( MaxConstrSign is arity-rich & MaxConstrSign is initialized )
thus ( MaxConstrSign is arity-rich & MaxConstrSign is initialized ) ; :: thesis: verum