let V be Z_Module; :: thesis: for W1, W2, W3 being strict Submodule of V st W1 is Submodule of W2 holds
W1 /\ W3 is Submodule of W2 /\ W3
let W1, W2, W3 be strict Submodule of V; :: thesis: ( W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3 )
set S = LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #);
reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3 as Element of LattStr(# (Submodules V),(SubJoin V),(SubMeet V) #) by VECTSP_5:def 3;
assume A1: W1 is Submodule of W2 ; :: thesis: W1 /\ W3 is Submodule of W2 /\ W3
A "\/" B = W1 + W2 by VECTSP_5:def 7
.= B by A1, Th98 ;
then A [= B ;
then A "/\" C [= B "/\" C by LATTICES:9;
then A2: (A "/\" C) "\/" (B "/\" C) = B "/\" C ;
A3: B "/\" C = W2 /\ W3 by VECTSP_5:def 8;
(A "/\" C) "\/" (B "/\" C) = (SubJoin V) . (((SubMeet V) . (A,C)),BC) by VECTSP_5:def 8
.= (SubJoin V) . (AC,BC) by VECTSP_5:def 8
.= (W1 /\ W3) + (W2 /\ W3) by VECTSP_5:def 7 ;
hence W1 /\ W3 is Submodule of W2 /\ W3 by A2, A3, Th98; :: thesis: verum