let X be non empty TopSpace; :: thesis: for A being Subset of
for Y being a_neighborhood of A holds A c= Y
let A be Subset of ; :: 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:44;
hence A c= Y by XBOOLE_1:1; :: thesis: verum