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