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