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

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

for v being Element of VS st v in C0 holds

a * v in C0

hence ex b_{1} being strict Subspace of VS st the carrier of b_{1} = meet ((carr VS) .: G)
by A5, VECTSP_4:34; :: thesis: verum

set C0 = meet cG;

A1: for X being set st X in (carr VS) .: G holds

0. VS in X

proof

(carr VS) .: G <> {}
by Th1;
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 A2, FUNCT_2:65;

A4: 0. VS in X1 by VECTSP_4:17;

X = the carrier of X1 by A3, Def4;

hence 0. VS in X by A4, STRUCT_0:def 5; :: thesis: verum

end;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 A2, FUNCT_2:65;

A4: 0. VS in X1 by VECTSP_4:17;

X = the carrier of X1 by A3, Def4;

hence 0. VS in X by A4, STRUCT_0:def 5; :: thesis: verum

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

for a being Element of F
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

hence v + u in C0 by A9, SETFAM_1:def 1; :: thesis: verum

end;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

(carr VS) .: G <> {}
by Th1;
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 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; :: thesis: verum

end;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 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; :: thesis: verum

hence v + u in C0 by A9, SETFAM_1:def 1; :: thesis: verum

for v being Element of VS st v in C0 holds

a * v in C0

proof

then
C0 is linearly-closed
by A6, VECTSP_4:def 1;
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

hence a * v in C0 by A18, SETFAM_1:def 1; :: thesis: verum

end;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

(carr VS) .: G <> {}
by Th1;
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 A17, SETFAM_1:def 1;

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 A19, FUNCT_2:65;

A22: X = the carrier of X1 by A21, Def4;

then v1 in X1 by A20, STRUCT_0:def 5;

then a * v1 in X1 by VECTSP_4:21;

hence a * v in X by A22, STRUCT_0:def 5; :: thesis: verum

end;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 A17, SETFAM_1:def 1;

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 A19, FUNCT_2:65;

A22: X = the carrier of X1 by A21, Def4;

then v1 in X1 by A20, STRUCT_0:def 5;

then a * v1 in X1 by VECTSP_4:21;

hence a * v in X by A22, STRUCT_0:def 5; :: thesis: verum

hence a * v in C0 by A18, SETFAM_1:def 1; :: thesis: verum

hence ex b