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

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