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;
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = Lin A by A2, VECTSP_7:def 3
.= (0). V by A4, MOD_3:6 ;
hence contradiction by A1, LMOD_6:7; :: thesis: verum