let R be Ring; :: thesis: for X, V being strict RightMod of R st V is Submodule of X & X is Submodule of V holds
V = X
let X, V be strict RightMod of R; :: thesis: ( V is Submodule of X & X is Submodule of V implies V = X )
assume that
A1: V is Submodule of X and
A2: X is Submodule of V ; :: thesis: V = X
set VX = the carrier of X;
set VV = the carrier of V;
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, A2, Def2;
then A3: the carrier of V = the carrier of X ;
set AX = the addF of X;
set AV = the addF of V;
( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X ) by A1, A2, Def2;
then A4: the addF of V = the addF of X by A3;
set MX = the rmult of X;
set MV = the rmult of V;
A5: the rmult of X = the rmult of V | [: the carrier of X, the carrier of R:] by A2, Def2;
( 0. V = 0. X & the rmult of V = the rmult of X | [: the carrier of V, the carrier of R:] ) by A1, Def2;
hence V = X by A3, A4, A5; :: thesis: verum