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
consider B being Subset of T such that
A2: B = {p} ` ;
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
A3: for C being Subset of T holds
( C in F iff S₁[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 ) )

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 ) )
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

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 ) ) )

proof

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;

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

end;

( 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
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;

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

end;

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

proof

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;

then A10: F c= 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 )

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 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;

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

proof

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;

then A15: B c= union F ;
for x being object st x in union F holds
x in B

proof

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;

then union F c= 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;

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

end;

assume A18: 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 ) )
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;

hence T is T_1 ; :: thesis: verum