set V = the LeftMod of R;
take (0). the LeftMod of R ; :: thesis: ( (0). the LeftMod of R is strict & (0). the LeftMod of R is free )
thus ( (0). the LeftMod of R is strict & (0). the LeftMod of R is free ) by Th14; :: thesis: verum