let K be Ring; :: thesis: for M, N being LeftMod of K st M c= N holds
(0). N c= M
let M, N be LeftMod of K; :: thesis: ( M c= N implies (0). N c= M )
assume M c= N ; :: thesis: (0). N c= M
then reconsider M' = M as Subspace of N by Def7;
(0). N is Subspace of M' by VECTSP_4:50;
hence (0). N c= M by Def7; :: thesis: verum