let R be Skew-Field; :: thesis: for V being LeftMod of R ex B being Subset of V st B is base
let V be LeftMod of R; :: thesis: ex B being Subset of V st B is base
ex B being Subset of V st
( {} the carrier of V c= B & B is base ) by Th26, LMOD_5:3;
hence ex B being Subset of V st B is base ; :: thesis: verum