let R be Ring; :: thesis: for V being trivial LeftMod of R holds (Omega). V = (0). V
let V be trivial LeftMod of R; :: thesis: (Omega). V = (0). V
assume (Omega). V <> (0). V ; :: thesis: contradiction
then consider v being Vector of V such that
A1: ( v in (Omega). V & v <> 0. V ) by ZMODUL04:24;
reconsider v = v as Vector of V ;
not V is trivial by A1;
hence contradiction ; :: thesis: verum