let F be Field; for V being VectSp of holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
let V be VectSp of ; LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th78;
reconsider S0 = S as 0_Lattice ;
reconsider S1 = S as 1_Lattice ;
consider W' being strict Subspace of V such that
A1:
the carrier of W' = the carrier of ((Omega). V)
;
reconsider I = W' as Element of by Def3;
reconsider I1 = I as Element of ;
reconsider Z = (0). V as Element of by Def3;
reconsider Z0 = Z as Element of ;
then A3:
Bottom S = Z
by RLSUB_2:84;
then A6:
Top S = I
by RLSUB_2:85;
now A7:
I is
Subspace of
(Omega). V
by Lm6;
let A be
Element of ;
ex B being Element of st B is_a_complement_of Aconsider W being
strict Subspace of
V such that A8:
W = A
by Def3;
consider L being
Linear_Compl of
W;
consider W'' being
strict Subspace of
V such that A9:
the
carrier of
W'' = the
carrier of
L
by Lm4;
reconsider B' =
W'' as
Element of
by Def3;
take B =
B';
B is_a_complement_of AA10:
B "/\" A =
(SubMeet V) . B,
A
by LATTICES:def 2
.=
W'' /\ W
by A8, Def8
.=
L /\ W
by A9, Lm8
.=
Bottom S
by A3, Th50
;
B "\/" A =
(SubJoin V) . B,
A
by LATTICES:def 1
.=
W'' + W
by A8, Def7
.=
L + W
by A9, Lm5
.=
VectSpStr(# the
carrier of
V,the
U7 of
V,the
U2 of
V,the
lmult of
V #)
by Th49
.=
Top S
by A1, A6, A7, VECTSP_4:39
;
hence
B is_a_complement_of A
by A10, LATTICES:def 18;
verum end;
hence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
by LATTICES:def 19; verum