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

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