let X be non empty TopSpace; :: thesis: for U1 being Subset of X
for x being Point of X st U1 is open & x in U1 holds
U1 is a_neighborhood of x
let U1 be Subset of X; :: thesis: for x being Point of X st U1 is open & x in U1 holds
U1 is a_neighborhood of x
let x be Point of X; :: thesis: ( U1 is open & x in U1 implies U1 is a_neighborhood of x )
assume ( U1 is open & x in U1 ) ; :: thesis: U1 is a_neighborhood of x
then x in Int U1 by TOPS_1:23;
hence U1 is a_neighborhood of x by Def1; :: thesis: verum