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