theorem :: RLTOPSP1:66

for X being LinearTopSpace ex P being local_base of X st P is circled-membered