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