let X be LinearTopSpace; :: thesis: for P being Subset-Family of X st P = { U where U is a_neighborhood of 0. X : verum } holds
P is local_base of X
let P be Subset-Family of X; :: thesis: ( P = { U where U is a_neighborhood of 0. X : verum } implies P is local_base of X )
assume A1: P = { U where U is a_neighborhood of 0. X : verum } ; :: thesis: P is local_base of X
let A 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= A )
take A ; :: thesis: ( A in P & A c= A )
thus ( A in P & A c= A ) by A1; :: thesis: verum