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 A1: ( K is trivial & not V is trivial ) ; :: thesis: contradiction
then ex a being Vector of V st a <> 0. V by STRUCT_0:def 19;
hence contradiction by A1, Th5; :: thesis: verum