take MaxConstrSign ; :: thesis: ( MaxConstrSign is initialized & MaxConstrSign is with_an_operation_for_each_sort & MaxConstrSign is strict )
thus ( MaxConstrSign is initialized & MaxConstrSign is with_an_operation_for_each_sort & MaxConstrSign is strict ) ; :: thesis: verum