let F be Field; for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
let V be VectSp of F; LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th60;
reconsider S0 = S as 0_Lattice ;
reconsider S1 = S as 1_Lattice ;
consider W9 being strict Subspace of V such that
A1:
the carrier of W9 = the carrier of ((Omega). V)
;
reconsider I = W9 as Element of S by Def3;
reconsider I1 = I as Element of S1 ;
reconsider Z = (0). V as Element of S by Def3;
reconsider Z0 = Z as Element of S0 ;
then A3:
Bottom S = Z
by RLSUB_2:64;
then A6:
Top S = I
by RLSUB_2:65;
now for A being Element of S ex B being Element of S st B is_a_complement_of AA7:
I is
Subspace of
(Omega). V
by Lm6;
let A be
Element of
S;
ex B being Element of S st B is_a_complement_of Aconsider W being
strict Subspace of
V such that A8:
W = A
by Def3;
set L = the
Linear_Compl of
W;
consider W99 being
strict Subspace of
V such that A9:
the
carrier of
W99 = the
carrier of the
Linear_Compl of
W
by Lm4;
reconsider B9 =
W99 as
Element of
S by Def3;
take B =
B9;
B is_a_complement_of AA10:
B "/\" A =
(SubMeet V) . (
B,
A)
by LATTICES:def 2
.=
W99 /\ W
by A8, Def8
.=
the
Linear_Compl of
W /\ W
by A9, Lm8
.=
Bottom S
by A3, Th40
;
B "\/" A =
(SubJoin V) . (
B,
A)
by LATTICES:def 1
.=
W99 + W
by A8, Def7
.=
the
Linear_Compl of
W + W
by A9, Lm5
.=
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #)
by Th39
.=
Top S
by A1, A6, A7, VECTSP_4:31
;
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