let R be non degenerated almost_left_invertible Ring; :: 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 VECTSP_7:17;
hence ex B being Subset of V st B is base ; :: thesis: verum