let T be non empty TopSpace; :: thesis: for A being Subset of T st ( for x being Point of T st x in A holds

A is Nbhd of x,T ) holds

A is open

let A be Subset of T; :: thesis: ( ( for x being Point of T st x in A holds

A is Nbhd of x,T ) implies A is open )

assume A1: for x being Point of T st x in A holds

A is Nbhd of x,T ; :: thesis: A is open

for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A

A is Nbhd of x,T ) holds

A is open

let A be Subset of T; :: thesis: ( ( for x being Point of T st x in A holds

A is Nbhd of x,T ) implies A is open )

assume A1: for x being Point of T st x in A holds

A is Nbhd of x,T ; :: thesis: A is open

for x being Point of T st x in A holds

ex B being Nbhd of x,T st B c= A

proof

hence
A is open
by Th17; :: thesis: verum
let x be Point of T; :: thesis: ( x in A implies ex B being Nbhd of x,T st B c= A )

assume A2: x in A ; :: thesis: ex B being Nbhd of x,T st B c= A

ex B being Nbhd of x,T st B c= A

end;assume A2: x in A ; :: thesis: ex B being Nbhd of x,T st B c= A

ex B being Nbhd of x,T st B c= A

proof

hence
ex B being Nbhd of x,T st B c= A
; :: thesis: verum
A is Nbhd of x,T
by A1, A2;

then consider B being Nbhd of x,T such that

A3: B = A ;

take B ; :: thesis: B c= A

thus B c= A by A3; :: thesis: verum

end;then consider B being Nbhd of x,T such that

A3: B = A ;

take B ; :: thesis: B c= A

thus B c= A by A3; :: thesis: verum