let X be LinearTopSpace; :: thesis: ( X is locally-convex implies ex P being local_base of X st P is convex-membered )
assume A1: X is locally-convex ; :: thesis: ex P being local_base of X st P is convex-membered
defpred S₁[ Subset of X] means ( $1 is circled & $1 is convex );
consider P being Subset-Family of X such that
A2: for V being Subset of X holds
( V in P iff S₁[V] ) from SUBSET_1:sch 3();
reconsider P = P as Subset-Family of X ;
take P ; :: thesis: ( P is local_base of X & P is convex-membered )
thus P is local_base of X :: thesis: P is convex-membered

proof

let V be a_neighborhood of 0. X; :: according to YELLOW13:def 2 :: thesis: ex b₁ being a_neighborhood of 0. X st
( b₁ in P & b₁ c= V )
consider Q being local_base of X such that
A3: Q is convex-membered by A1, Def11;
consider U being a_neighborhood of 0. X such that
A4: U in Q and
A5: U c= V by YELLOW13:def 2;
U is convex by A3, A4, Def3;
then consider W being a_neighborhood of 0. X such that
A6: ( W is circled & W is convex ) and
A7: W c= U by Th66;
take W ; :: thesis: ( W in P & W c= V )
thus W in P by A2, A6; :: thesis: W c= V
thus W c= V by A5, A7, XBOOLE_1:1; :: thesis: verum

end;

let V be Subset of X; :: according to RLTOPSP1:def 3 :: thesis: ( V in P implies V is convex )
assume V in P ; :: thesis: V is convex
hence V is convex by A2; :: thesis: verum