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 A1: A c= B ; :: thesis: B is a_neighborhood of x
A2: x in Int A by CONNSP_2:def 1;
Int A c= Int B by A1, TOPS_1:48;
hence B is a_neighborhood of x by A2, CONNSP_2:def 1; :: thesis: verum