let F be Subset-Family of T; :: thesis: ( F is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A ) )

hereby :: thesis: ( ( for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A ) ) implies F is basis of p )

assume A1: F is basis of p ; :: thesis: for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A )
let A be a_neighborhood of p; :: thesis: ex P being a_neighborhood of p st
( P in F & P c= A )
p in Int A by CONNSP_2:def 1;
then consider P being Subset of T such that
A2: P in F and
A3: p in Int P and
A4: P c= A by A1, Def1;
reconsider P = P as a_neighborhood of p by A3, CONNSP_2:def 1;
take P = P; :: thesis: ( P in F & P c= A )
thus ( P in F & P c= A ) by A2, A4; :: thesis: verum

end;

assume A5: for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A ) ; :: thesis: F is basis of p
let A be Subset of T; :: according to YELLOW13:def 1 :: thesis: ( p in Int A implies ex P being Subset of T st
( P in F & p in Int P & P c= A ) )
assume p in Int A ; :: thesis: ex P being Subset of T st
( P in F & p in Int P & P c= A )
then A is a_neighborhood of p by CONNSP_2:def 1;
then consider P being a_neighborhood of p such that
A6: ( P in F & P c= A ) by A5;
take P ; :: thesis: ( P in F & p in Int P & P c= A )
thus ( P in F & p in Int P & P c= A ) by A6, CONNSP_2:def 1; :: thesis: verum