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