consider S being strict Submodule of RightModule R such that
A1: the carrier of S = P by Lm10;
reconsider T = RightModStr(# the carrier of S, the addF of S, the ZeroF of S, the rmult of S #) as Submodule of P by A1, Def15;
take T ; :: thesis: T is strict
thus T is strict ; :: thesis: verum