take maxnorm ; :: thesis: ( maxnorm is commutative & maxnorm is associative & maxnorm is monotonic & maxnorm is with-0-identity )
thus ( maxnorm is commutative & maxnorm is associative & maxnorm is monotonic & maxnorm is with-0-identity ) ; :: thesis: verum