let V be RealLinearSpace; :: thesis: for W1, W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds

W1 /\ W3 is Subspace of W2 /\ W3

let W1, W2, W3 be strict Subspace of V; :: thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 )

set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);

reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

assume A1: W1 is Subspace of W2 ; :: thesis: W1 /\ W3 is Subspace of W2 /\ W3

A "\/" B = W1 + W2 by Def7

.= B by A1, Th8 ;

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 Def8;

(A "/\" C) "\/" (B "/\" C) = (SubJoin V) . (((SubMeet V) . (A,C)),BC) by Def8

.= (SubJoin V) . (AC,BC) by Def8

.= (W1 /\ W3) + (W2 /\ W3) by Def7 ;

hence W1 /\ W3 is Subspace of W2 /\ W3 by A2, A3, Th8; :: thesis: verum

W1 /\ W3 is Subspace of W2 /\ W3

let W1, W2, W3 be strict Subspace of V; :: thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 )

set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);

reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;

assume A1: W1 is Subspace of W2 ; :: thesis: W1 /\ W3 is Subspace of W2 /\ W3

A "\/" B = W1 + W2 by Def7

.= B by A1, Th8 ;

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 Def8;

(A "/\" C) "\/" (B "/\" C) = (SubJoin V) . (((SubMeet V) . (A,C)),BC) by Def8

.= (SubJoin V) . (AC,BC) by Def8

.= (W1 /\ W3) + (W2 /\ W3) by Def7 ;

hence W1 /\ W3 is Subspace of W2 /\ W3 by A2, A3, Th8; :: thesis: verum