let X be LinearTopSpace; :: thesis: ex P being local_base of X st P is circled-membered
defpred S₁[ Subset of X] means $1 is circled ;
consider P being Subset-Family of X such that
A1: 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 circled-membered )
thus P is local_base of X :: thesis: P is circled-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 W being a_neighborhood of 0. X such that
A2: W is circled and
A3: W c= V by Th64;
take W ; :: thesis: ( W in P & W c= V )
thus W in P by A1, A2; :: thesis: W c= V
thus W c= V by A3; :: thesis: verum

end;

let V be Subset of X; :: according to RLTOPSP1:def 7 :: thesis: ( V in P implies V is circled )
assume V in P ; :: thesis: V is circled
hence V is circled by A1; :: thesis: verum