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
proof
let X be set ; :: thesis: ( X in (carr VS) .: G implies 0. VS in X )
assume A2: X in (carr VS) .: G ; :: thesis: 0. VS in X
then reconsider X = X as Subset of VS ;
consider X1 being Element of Subspaces VS such that
X1 in G and
A3: X = (carr VS) . X1 by ;
A4: 0. VS in X1 by VECTSP_4:17;
X = the carrier of X1 by ;
hence 0. VS in X by ; :: thesis: verum
end;
(carr VS) .: G <> {} by Th1;
then A5: meet cG <> {} by ;
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; :: thesis: ( v in C0 & u in C0 implies v + u in C0 )
assume that
A7: v in C0 and
A8: u in C0 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: v + u in X
then A11: v in X by ;
A12: u in X by ;
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 ;
A14: X = the carrier of X1 by ;
then A15: u1 in X1 by ;
consider X2 being strict Subspace of VS such that
A16: X2 = X1 by VECTSP_5:def 3;
v1 in X1 by ;
then vu in X1 + X1 by ;
then vu in X2 by ;
hence v + u in X by ; :: thesis: verum
end;
(carr VS) .: G <> {} by Th1;
hence v + u in C0 by ; :: thesis: verum
end;
for a being Element of F
for v being Element of VS st v in C0 holds
a * v in C0
proof
let a be Element of F; :: thesis: for v being Element of VS st v in C0 holds
a * v in C0

let v be Element of VS; :: thesis: ( v in C0 implies a * v in C0 )
assume A17: v in C0 ; :: thesis: a * v in C0
A18: for X being set st X in (carr VS) .: G holds
a * v in X
proof
reconsider v1 = v as Element of VS ;
let X be set ; :: thesis: ( X in (carr VS) .: G implies a * v in X )
assume A19: X in (carr VS) .: G ; :: thesis: a * v in X
then A20: v in X by ;
reconsider X = X as Subset of VS by A19;
consider X1 being Element of Subspaces VS such that
X1 in G and
A21: X = (carr VS) . X1 by ;
A22: X = the carrier of X1 by ;
then v1 in X1 by ;
then a * v1 in X1 by VECTSP_4:21;
hence a * v in X by ; :: thesis: verum
end;
(carr VS) .: G <> {} by Th1;
hence a * v in C0 by ; :: thesis: verum
end;
then C0 is linearly-closed by ;
hence ex b1 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G) by ; :: thesis: verum