let K be Ring; :: thesis: for V being LeftMod of K st not V is trivial holds
for A being Subset of V st A is base holds
A <> {}
let V be LeftMod of K; :: thesis: ( not V is trivial implies for A being Subset of V st A is base holds
A <> {} )
assume A1: not V is trivial ; :: thesis: for A being Subset of V st A is base holds
A <> {}
let A be Subset of V; :: thesis: ( A is base implies A <> {} )
assume that
A2: A is base and
A3: A = {} ; :: thesis: contradiction
A4: A = {} the carrier of V by A3;
VectSpStr(# the carrier of V,the addF of V,the ZeroF of V,the lmult of V #) = Lin A by A2, MOD_3:def 2
.= (0). V by A4, MOD_3:13 ;
hence contradiction by A1, LMOD_6:7; :: thesis: verum