reconsider cG = (carr VS) .: G as Subset-Family of VS ;
set C0 = meet cG;
A1:
for X being set st X in (carr VS) .: G holds
0. VS in X
(carr VS) .: G <> {}
by Th1;
then A5:
meet cG <> {}
by A1, SETFAM_1:def 1;
reconsider C0 = meet cG as Subset of VS ;
A6:
for v, u being Element of VS st v in C0 & u in C0 holds
v + u in C0
proof
let v,
u be
Element of
VS;
( v in C0 & u in C0 implies v + u in C0 )
assume that A7:
v in C0
and A8:
u in C0
;
v + u in C0
A9:
for
X being
set st
X in (carr VS) .: G holds
v + u in X
proof
reconsider v1 =
v,
u1 =
u as
Element of
VS ;
let X be
set ;
( X in (carr VS) .: G implies v + u in X )
reconsider vu =
v1 + u1 as
Element of
VS ;
assume A10:
X in (carr VS) .: G
;
v + u in X
then A11:
v in X
by A7, SETFAM_1:def 1;
A12:
u in X
by A8, A10, SETFAM_1:def 1;
reconsider X =
X as
Subset of
VS by A10;
consider X1 being
Element of
Subspaces VS such that
X1 in G
and A13:
X = (carr VS) . X1
by A10, FUNCT_2:65;
A14:
X = the
carrier of
X1
by A13, Def4;
then A15:
u1 in X1
by A12, STRUCT_0:def 5;
consider X2 being
strict Subspace of
VS such that A16:
X2 = X1
by VECTSP_5:def 3;
v1 in X1
by A11, A14, STRUCT_0:def 5;
then
vu in X1 + X1
by A15, VECTSP_5:1;
then
vu in X2
by A16, VECTSP_5:4;
hence
v + u in X
by A14, A16, STRUCT_0:def 5;
verum
end;
(carr VS) .: G <> {}
by Th1;
hence
v + u in C0
by A9, SETFAM_1:def 1;
verum
end;
for a being Element of F
for v being Element of VS st v in C0 holds
a * v in C0
then
C0 is linearly-closed
by A6, VECTSP_4:def 1;
hence
ex b1 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G)
by A5, VECTSP_4:34; verum