let X be non empty TopSpace; :: thesis: for x being Point of X
for A being a_neighborhood of x
for B being Subset of X st A c= B holds
B is a_neighborhood of x
let x be Point of X; :: thesis: for A being a_neighborhood of x
for B being Subset of X st A c= B holds
B is a_neighborhood of x
let A be a_neighborhood of x; :: thesis: for B being Subset of X st A c= B holds
B is a_neighborhood of x
let B be Subset of X; :: thesis: ( A c= B implies B is a_neighborhood of x )
assume A c= B ; :: thesis: B is a_neighborhood of x
then ( x in Int A & Int A c= Int B ) by CONNSP_2:def 1, TOPS_1:19;
hence B is a_neighborhood of x by CONNSP_2:def 1; :: thesis: verum