let X be RealLinearSpace; :: thesis: for B being Basis of X holds not 0. X in B
let B be Basis of X; :: thesis: not 0. X in B
assume 0. X in B ; :: thesis: contradiction
then {(0. X)} c= B by ZFMISC_1:31;
then {(0. X)} is linearly-independent by RLVECT_3:def 3, RLVECT_3:5;
hence contradiction by RLVECT_3:9; :: thesis: verum