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

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