let V be RealUnitarySpace; 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; ( 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
; W1 /\ W3 is Subspace of W2 /\ W3
A "\/" B =
(SubJoin V) . (A,B)
by LATTICES:def 1
.=
W1 + W2
by Def7
.=
B
by A1, Th8
;
then
A [= B
by LATTICES:def 3;
then
A "/\" C [= B "/\" C
by LATTICES:9;
then A2:
(A "/\" C) "\/" (B "/\" C) = B "/\" C
by LATTICES:def 3;
A3: B "/\" C =
(SubMeet V) . (B,C)
by LATTICES:def 2
.=
W2 /\ W3
by Def8
;
(A "/\" C) "\/" (B "/\" C) =
(SubJoin V) . ((A "/\" C),(B "/\" C))
by LATTICES:def 1
.=
(SubJoin V) . (((SubMeet V) . (A,C)),(B "/\" C))
by LATTICES:def 2
.=
(SubJoin V) . (((SubMeet V) . (A,C)),((SubMeet V) . (B,C)))
by LATTICES:def 2
.=
(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; verum