let K be Ring; :: thesis: for V being LeftMod of K st K is trivial holds
V is trivial
let V be LeftMod of K; :: thesis: ( K is trivial implies V is trivial )
assume that
A1: K is trivial and
A2: not V is trivial ; :: thesis: contradiction
ex a being Vector of V st a <> 0. V by A2, STRUCT_0:def 18;
hence contradiction by A1, Th5; :: thesis: verum