ex S being strict Submodule of RightModule R st the carrier of S = P by Lm10;
hence ex b₁ being Submodule of RightModule R st the carrier of b₁ = P ; :: thesis: verum