theorem :: MONOID_0:57

multnat = multreal || NAT by Th24, Th52;