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

for Y being a_neighborhood of A holds A c= Y

let A be Subset of X; :: thesis: for Y being a_neighborhood of A holds A c= Y

let Y be a_neighborhood of A; :: thesis: A c= Y

( A c= Int Y & Int Y c= Y ) by Def2, TOPS_1:16;

hence A c= Y ; :: thesis: verum

for Y being a_neighborhood of A holds A c= Y

let A be Subset of X; :: thesis: for Y being a_neighborhood of A holds A c= Y

let Y be a_neighborhood of A; :: thesis: A c= Y

( A c= Int Y & Int Y c= Y ) by Def2, TOPS_1:16;

hence A c= Y ; :: thesis: verum