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