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