(0). (LeftModule R) is free by Th21;
hence ex b₁ being LeftMod of R st
( b₁ is strict & b₁ is free ) ; :: thesis: verum