Theorem Set.Nonempty.mul

Modification history