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