let X be LinearTopSpace; :: thesis: for U being a_neighborhood of 0. X st U is convex holds
ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
let U be a_neighborhood of 0. X; :: thesis: ( U is convex implies ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U ) )
assume A1: U is convex ; :: thesis: ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
set V = U /\ (- U);
- U is a_neighborhood of 0. X by Th56;
then reconsider V = U /\ (- U) as a_neighborhood of 0. X by CONNSP_2:2;
take V ; :: thesis: ( V is circled & V is convex & V c= U )
A2: - U is convex by A1, CONVEX1:1;
thus V is circled :: thesis: ( V is convex & V c= U )

proof

0. X in V by CONNSP_2:4;
then A3: 0. X in - U by XBOOLE_0:def 4;
A4: 0. X in U by CONNSP_2:4;
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( abs r <= 1 implies r * V c= V )
assume A5: abs r <= 1 ; :: thesis: r * V c= V
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in r * V or u in V )
assume u in r * V ; :: thesis: u in V
then consider v being Point of X such that
A6: u = r * v and
A7: v in V ;
A8: v in - U by A7, XBOOLE_0:def 4;
A9: v in U by A7, XBOOLE_0:def 4;

per cases ( r < 0 or r >= 0 ) ;

suppose A10: r < 0 ; :: thesis: u in V

then A11: - r <= 1 by A5, ABSVALUE:def 1;
then ((- r) * v) + ((1 - (- r)) * (0. X)) in - U by A2, A8, A3, A10, Def1;
then ((- r) * v) + (0. X) in - U by RLVECT_1:10;
then (- r) * v in - U by RLVECT_1:def 4;
then consider u9 being Point of X such that
A12: (- r) * v = (- 1) * u9 and
A13: u9 in U ;
((- r) * v) + ((1 - (- r)) * (0. X)) in U by A1, A9, A4, A10, A11, Def1;
then ((- r) * v) + (0. X) in U by RLVECT_1:10;
then (- r) * v in U by RLVECT_1:def 4;
then (- 1) * (((- 1) * r) * v) in (- 1) * U ;
then A14: ((- 1) * ((- 1) * r)) * v in (- 1) * U by RLVECT_1:def 7;
u9 = ((- 1) * (- 1)) * u9 by RLVECT_1:def 8
.= (- 1) * ((- 1) * u9) by RLVECT_1:def 7
.= ((- r) * (- 1)) * v by A12, RLVECT_1:def 7
.= r * v ;
hence u in V by A6, A13, A14, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A15: r >= 0 ; :: thesis: u in V

A16: r <= 1 by A5, ABSVALUE:def 1;
then (r * v) + ((1 - r) * (0. X)) in - U by A2, A8, A3, A15, Def1;
then (r * v) + (0. X) in - U by RLVECT_1:10;
then A17: r * v in - U by RLVECT_1:def 4;
(r * v) + ((1 - r) * (0. X)) in U by A1, A9, A4, A15, A16, Def1;
then (r * v) + (0. X) in U by RLVECT_1:10;
then r * v in U by RLVECT_1:def 4;
hence u in V by A6, A17, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

thus V is convex by A1, A2; :: thesis: V c= U
thus V c= U by XBOOLE_1:17; :: thesis: verum