let T be non empty TopSpace; 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; ( ( 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
; 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
let x be
Point of
T;
( x in A implies ex B being Nbhd of x,T st B c= A )
assume A2:
x in A
;
ex B being Nbhd of x,T st B c= A
ex
B being
Nbhd of
x,
T st
B c= A
proof
A is
Nbhd of
x,
T
by A1, A2;
then consider B being
Nbhd of
x,
T such that A3:
B = A
;
take
B
;
B c= A
thus
B c= A
by A3;
verum
end;
hence
ex
B being
Nbhd of
x,
T st
B c= A
;
verum
end;
hence
A is open
by Th17; verum