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 that
A1: V c= M and
A2: M c= V ; :: thesis: V = M
A3: V is Subspace of M by A1, Def7;
M is Subspace of V by A2, Def7;
hence V = M by A3, VECTSP_4:33; :: thesis: verum