let R be Ring; :: thesis: for V being RightMod of R
for W being Submodule of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let V be RightMod of R; :: thesis: for W being Submodule of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let W be Submodule of V; :: thesis: ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
0. V in W by RMOD_2:17;
then 0. V in the carrier of W ;
then {(0. V)} c= the carrier of W by ZFMISC_1:31;
then A1: {(0. V)} /\ the carrier of W = {(0. V)} by XBOOLE_1:28;
the carrier of (((0). V) /\ W) = the carrier of ((0). V) /\ the carrier of W by Def2
.= {(0. V)} /\ the carrier of W by RMOD_2:def 3 ;
hence ((0). V) /\ W = (0). V by A1, RMOD_2:def 3; :: thesis: W /\ ((0). V) = (0). V
hence W /\ ((0). V) = (0). V by Th14; :: thesis: verum