let X be non empty TopSpace; :: thesis: for A, B being Subset of X

for U being a_neighborhood of B st A c= B holds

U is a_neighborhood of A

let A, B be Subset of X; :: thesis: for U being a_neighborhood of B st A c= B holds

U is a_neighborhood of A

let U be a_neighborhood of B; :: thesis: ( A c= B implies U is a_neighborhood of A )

assume A1: A c= B ; :: thesis: U is a_neighborhood of A

B c= Int U by CONNSP_2:def 2;

hence A c= Int U by A1; :: according to CONNSP_2:def 2 :: thesis: verum

for U being a_neighborhood of B st A c= B holds

U is a_neighborhood of A

let A, B be Subset of X; :: thesis: for U being a_neighborhood of B st A c= B holds

U is a_neighborhood of A

let U be a_neighborhood of B; :: thesis: ( A c= B implies U is a_neighborhood of A )

assume A1: A c= B ; :: thesis: U is a_neighborhood of A

B c= Int U by CONNSP_2:def 2;

hence A c= Int U by A1; :: according to CONNSP_2:def 2 :: thesis: verum