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