theorem :: ZMODUL08:5

ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) is Submodule of Rat-Module