let K be Ring; :: thesis: for V, M, N being LeftMod of K st V c= M & M c= N holds
V c= N
let V, M, N be LeftMod of K; :: thesis: ( V c= M & M c= N implies V c= N )
assume ( V c= M & M c= N ) ; :: thesis: V c= N
then ( V is Subspace of M & M is Subspace of N ) by Def7;
then V is Subspace of N by VECTSP_4:34;
hence V c= N by Def7; :: thesis: verum