let T be non empty TopSpace; :: thesis: ( T is T_1 iff for p being Point of T holds {p} is closed )

thus ( T is T_1 implies for p being Point of T holds {p} is closed ) :: thesis: ( ( for p being Point of T holds {p} is closed ) implies T is T_1 )

for p, q being Point of T st not p = q holds

ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V )

thus ( T is T_1 implies for p being Point of T holds {p} is closed ) :: thesis: ( ( for p being Point of T holds {p} is closed ) implies T is T_1 )

proof

assume A18:
for p being Point of T holds {p} is closed
; :: thesis: T is T_1
assume A1:
T is T_1
; :: thesis: for p being Point of T holds {p} is closed

for p being Point of T holds {p} is closed

end;for p being Point of T holds {p} is closed

proof

hence
for p being Point of T holds {p} is closed
; :: thesis: verum
let p be Point of T; :: thesis: {p} is closed

consider B being Subset of T such that

A2: B = {p} ` ;

defpred S_{1}[ Subset of T] means ex q being Point of T st

( q in B & ( for V being Subset of T st $1 = V holds

( V is open & q in V & not p in V ) ) );

consider F being Subset-Family of T such that

A3: for C being Subset of T holds

( C in F iff S_{1}[C] )
from SUBSET_1:sch 3();

A4: for C being Subset of T holds

( C in F iff ex q being Point of T st

( q in B & C is open & q in C & not p in C ) )

x in the topology of T

A11: for q being Point of T st q in B holds

ex V being Subset of T st

( V is open & q in V & not p in V )

x in union F

for x being object st x in union F holds

x in B

then B = union F by A15;

then B in the topology of T by A10, PRE_TOPC:def 1;

then ( {p} ` = ([#] T) \ {p} & B is open ) ;

hence {p} is closed by A2; :: thesis: verum

end;consider B being Subset of T such that

A2: B = {p} ` ;

defpred S

( q in B & ( for V being Subset of T st $1 = V holds

( V is open & q in V & not p in V ) ) );

consider F being Subset-Family of T such that

A3: for C being Subset of T holds

( C in F iff S

A4: for C being Subset of T holds

( C in F iff ex q being Point of T st

( q in B & C is open & q in C & not p in C ) )

proof

for x being object st x in F holds
let C be Subset of T; :: thesis: ( C in F iff ex q being Point of T st

( q in B & C is open & q in C & not p in C ) )

A5: ( ex q being Point of T st

( q in B & C is open & q in C & not p in C ) implies C in F )

( q in B & C is open & q in C & not p in C ) )

( q in B & C is open & q in C & not p in C ) ) by A5; :: thesis: verum

end;( q in B & C is open & q in C & not p in C ) )

A5: ( ex q being Point of T st

( q in B & C is open & q in C & not p in C ) implies C in F )

proof

( C in F implies ex q being Point of T st
assume A6:
ex q being Point of T st

( q in B & C is open & q in C & not p in C ) ; :: thesis: C in F

ex q being Point of T st

( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) )

end;( q in B & C is open & q in C & not p in C ) ; :: thesis: C in F

ex q being Point of T st

( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) )

proof

hence
C in F
by A3; :: thesis: verum
consider q being Point of T such that

A7: ( q in B & C is open & q in C & not p in C ) by A6;

take q ; :: thesis: ( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) )

thus ( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) ) by A7; :: thesis: verum

end;A7: ( q in B & C is open & q in C & not p in C ) by A6;

take q ; :: thesis: ( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) )

thus ( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) ) by A7; :: thesis: verum

( q in B & C is open & q in C & not p in C ) )

proof

hence
( C in F iff ex q being Point of T st
assume
C in F
; :: thesis: ex q being Point of T st

( q in B & C is open & q in C & not p in C )

then consider q being Point of T such that

A8: ( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) ) by A3;

take q ; :: thesis: ( q in B & C is open & q in C & not p in C )

thus ( q in B & C is open & q in C & not p in C ) by A8; :: thesis: verum

end;( q in B & C is open & q in C & not p in C )

then consider q being Point of T such that

A8: ( q in B & ( for V being Subset of T st C = V holds

( V is open & q in V & not p in V ) ) ) by A3;

take q ; :: thesis: ( q in B & C is open & q in C & not p in C )

thus ( q in B & C is open & q in C & not p in C ) by A8; :: thesis: verum

( q in B & C is open & q in C & not p in C ) ) by A5; :: thesis: verum

x in the topology of T

proof

then A10:
F c= the topology of T
;
let x be object ; :: thesis: ( x in F implies x in the topology of T )

assume A9: x in F ; :: thesis: x in the topology of T

then reconsider x = x as Subset of T ;

ex q being Point of T st

( q in B & x is open & q in x & not p in x ) by A4, A9;

hence x in the topology of T ; :: thesis: verum

end;assume A9: x in F ; :: thesis: x in the topology of T

then reconsider x = x as Subset of T ;

ex q being Point of T st

( q in B & x is open & q in x & not p in x ) by A4, A9;

hence x in the topology of T ; :: thesis: verum

A11: for q being Point of T st q in B holds

ex V being Subset of T st

( V is open & q in V & not p in V )

proof

for x being object st x in B holds
let q be Point of T; :: thesis: ( q in B implies ex V being Subset of T st

( V is open & q in V & not p in V ) )

assume q in B ; :: thesis: ex V being Subset of T st

( V is open & q in V & not p in V )

then not q in {p} by A2, XBOOLE_0:def 5;

then not q = p by TARSKI:def 1;

then ex V, W being Subset of T st

( V is open & W is open & q in V & not p in V & p in W & not q in W ) by A1;

then consider V being Subset of T such that

A12: ( V is open & q in V & not p in V ) ;

take V ; :: thesis: ( V is open & q in V & not p in V )

thus ( V is open & q in V & not p in V ) by A12; :: thesis: verum

end;( V is open & q in V & not p in V ) )

assume q in B ; :: thesis: ex V being Subset of T st

( V is open & q in V & not p in V )

then not q in {p} by A2, XBOOLE_0:def 5;

then not q = p by TARSKI:def 1;

then ex V, W being Subset of T st

( V is open & W is open & q in V & not p in V & p in W & not q in W ) by A1;

then consider V being Subset of T such that

A12: ( V is open & q in V & not p in V ) ;

take V ; :: thesis: ( V is open & q in V & not p in V )

thus ( V is open & q in V & not p in V ) by A12; :: thesis: verum

x in union F

proof

then A15:
B c= union F
;
let x be object ; :: thesis: ( x in B implies x in union F )

assume A13: x in B ; :: thesis: x in union F

then reconsider x = x as Point of T ;

consider C being Subset of T such that

A14: ( C is open & x in C & not p in C ) by A11, A13;

ex C being set st

( x in C & C in F ) by A4, A13, A14;

hence x in union F by TARSKI:def 4; :: thesis: verum

end;assume A13: x in B ; :: thesis: x in union F

then reconsider x = x as Point of T ;

consider C being Subset of T such that

A14: ( C is open & x in C & not p in C ) by A11, A13;

ex C being set st

( x in C & C in F ) by A4, A13, A14;

hence x in union F by TARSKI:def 4; :: thesis: verum

for x being object st x in union F holds

x in B

proof

then
union F c= B
;
let x be object ; :: thesis: ( x in union F implies x in B )

assume x in union F ; :: thesis: x in B

then consider C being set such that

A16: x in C and

A17: C in F by TARSKI:def 4;

reconsider C = C as Subset of T by A17;

ex q being Point of T st

( q in B & C is open & q in C & not p in C ) by A4, A17;

then C c= ([#] T) \ {p} by ZFMISC_1:34;

hence x in B by A2, A16; :: thesis: verum

end;assume x in union F ; :: thesis: x in B

then consider C being set such that

A16: x in C and

A17: C in F by TARSKI:def 4;

reconsider C = C as Subset of T by A17;

ex q being Point of T st

( q in B & C is open & q in C & not p in C ) by A4, A17;

then C c= ([#] T) \ {p} by ZFMISC_1:34;

hence x in B by A2, A16; :: thesis: verum

then B = union F by A15;

then B in the topology of T by A10, PRE_TOPC:def 1;

then ( {p} ` = ([#] T) \ {p} & B is open ) ;

hence {p} is closed by A2; :: thesis: verum

for p, q being Point of T st not p = q holds

ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V )

proof

hence
T is T_1
; :: thesis: verum
let p, q be Point of T; :: thesis: ( not p = q implies ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V ) )

consider V, W being Subset of T such that

A19: V = {p} ` and

A20: W = {q} ` ;

p in {p} by TARSKI:def 1;

then A21: not p in V by A19, XBOOLE_0:def 5;

assume A22: not p = q ; :: thesis: ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V )

then not p in {q} by TARSKI:def 1;

then A23: p in W by A20, XBOOLE_0:def 5;

q in {q} by TARSKI:def 1;

then A24: not q in W by A20, XBOOLE_0:def 5;

not q in {p} by A22, TARSKI:def 1;

then A25: q in V by A19, XBOOLE_0:def 5;

( {p} is closed & {q} is closed ) by A18;

hence ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V ) by A19, A20, A23, A24, A25, A21; :: thesis: verum

end;( W is open & V is open & p in W & not q in W & q in V & not p in V ) )

consider V, W being Subset of T such that

A19: V = {p} ` and

A20: W = {q} ` ;

p in {p} by TARSKI:def 1;

then A21: not p in V by A19, XBOOLE_0:def 5;

assume A22: not p = q ; :: thesis: ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V )

then not p in {q} by TARSKI:def 1;

then A23: p in W by A20, XBOOLE_0:def 5;

q in {q} by TARSKI:def 1;

then A24: not q in W by A20, XBOOLE_0:def 5;

not q in {p} by A22, TARSKI:def 1;

then A25: q in V by A19, XBOOLE_0:def 5;

( {p} is closed & {q} is closed ) by A18;

hence ex W, V being Subset of T st

( W is open & V is open & p in W & not q in W & q in V & not p in V ) by A19, A20, A23, A24, A25, A21; :: thesis: verum