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 )

proof

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

proof

let p be Point of T; :: thesis: {p} is closed
A2: {p} ` = ([#] T) \ {p} ;
consider B being Subset of T such that
A3: B = {p} ` ;
A4: 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

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 ( q in [#] T & not q in {p} ) by A3, XBOOLE_0:def 5;
then ( q in [#] T & 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, Def9;
then consider V being Subset of T such that
A5: ( 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 A5; :: thesis: verum

end;

defpred S₁[ 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
A6: for C being Subset of T holds
( C in F iff S₁[C] ) from SUBSET_1:sch 3();
A7: 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

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 ) )
A8: ( C in F implies ex q being Point of T st
( q in B & C is open & q in C & not p in C ) )

proof

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
A9: ( q in B & ( for V being Subset of T st C = V holds
( V is open & q in V & not p in V ) ) ) by A6;
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 A9; :: thesis: verum

end;

( 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

assume A10: 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 ) ) )

proof

consider q being Point of T such that
A11: ( q in B & C is open & q in C & not p in C ) by A10;
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 A11; :: thesis: verum

end;

hence C in F by A6; :: thesis: verum

end;

hence ( C in F iff ex q being Point of T st
( q in B & C is open & q in C & not p in C ) ) by A8; :: thesis: verum

end;

A12: B = union F

proof

A13: B c= union F

proof

for x being set st x in B holds
x in union F

proof

let x be set ; :: thesis: ( x in B implies x in union F )
assume A14: x in B ; :: thesis: x in union F
then reconsider x = x as Point of T ;
consider C being Subset of T such that
A15: ( C is open & x in C & not p in C ) by A4, A14;
ex C being set st
( x in C & C in F )

proof

take C ; :: thesis: ( x in C & C in F )
thus ( x in C & C in F ) by A7, A14, A15; :: thesis: verum

end;

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

end;

hence B c= union F by TARSKI:def 3; :: thesis: verum

end;

union F c= B

proof

for x being set st x in union F holds
x in B

proof

let x be set ; :: 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 & C in F ) by TARSKI:def 4;
reconsider C = C as Subset of T by A16;
consider q being Point of T such that
A17: ( q in B & C is open & q in C & not p in C ) by A7, A16;
C c= ([#] T) \ {p} by A17, ZFMISC_1:40;
hence x in B by A3, A16; :: thesis: verum

end;

hence union F c= B by TARSKI:def 3; :: thesis: verum

end;

hence B = union F by A13, XBOOLE_0:def 10; :: thesis: verum

end;

F c= the topology of T

proof

for x being set st x in F holds
x in the topology of T

proof

let x be set ; :: thesis: ( x in F implies x in the topology of T )
assume A18: x in F ; :: thesis: x in the topology of T
then reconsider x = x as Subset of T ;
consider q being Point of T such that
A19: ( q in B & x is open & q in x & not p in x ) by A7, A18;
thus x in the topology of T by A19, PRE_TOPC:def 5; :: thesis: verum

end;

hence F c= the topology of T by TARSKI:def 3; :: thesis: verum

end;

then B in the topology of T by A12, PRE_TOPC:def 1;
then B is open by PRE_TOPC:def 5;
hence {p} is closed by A2, A3, PRE_TOPC:def 6; :: thesis: verum

end;

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

end;

assume A20: for p being Point of T holds {p} is closed ; :: thesis: 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 )

proof

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 ) )
assume A21: 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 )
consider V, W being Subset of T such that
A23: ( V = {p} ` & W = {q} ` ) ;
( {p} is closed & {q} is closed ) by A20;
then A24: ( V is open & W is open ) by A23;
( p in W & not q in W & q in V & not p in V )

proof

A25: ( not p in {q} & not q in {p} ) by A21, TARSKI:def 1;
( p in {p} & q in {q} ) by TARSKI:def 1;
hence ( p in W & not q in W & q in V & not p in V ) by A23, A25, XBOOLE_0:def 5; :: thesis: verum

end;

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 A24; :: thesis: verum

end;

hence T is T_1 by Def9; :: thesis: verum