let T be non empty TopSpace; :: thesis: T_1-reflex T is T_1

now :: thesis: for p being Point of (T_1-reflex T) holds {p} is closed

hence
T_1-reflex T is T_1
by URYSOHN1:19; :: thesis: verumlet p be Point of (T_1-reflex T); :: thesis: {p} is closed

reconsider I = (Intersection (Closed_Partitions T)) \ {p} as Subset of (Intersection (Closed_Partitions T)) by XBOOLE_1:36;

A1: the carrier of (T_1-reflex T) = Intersection (Closed_Partitions T) by BORSUK_1:def 7;

then consider x being Element of T such that

A2: p = EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:42;

reconsider q = p as Subset of T by A2;

A3: { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } c= bool the carrier of T

reconsider m = m as non empty Subset-Family of T ;

A5: for A being Subset of T st A in m holds

A is closed

then q is closed by A5, PRE_TOPC:14;

then ([#] T) \ q is open ;

then A7: ([#] T) \ p in the topology of T ;

p in Intersection (Closed_Partitions T) by A1;

then union ((Intersection (Closed_Partitions T)) \ {p}) in the topology of T by A7, EQREL_1:44;

then A8: I in { A where A is Subset of (Intersection (Closed_Partitions T)) : union A in the topology of T } ;

reconsider I = I as Subset of (space (Intersection (Closed_Partitions T))) by BORSUK_1:def 7;

reconsider I = I as Subset of (T_1-reflex T) ;

( the topology of (space (Intersection (Closed_Partitions T))) = { A where A is Subset of (Intersection (Closed_Partitions T)) : union A in the topology of T } & I = ([#] (T_1-reflex T)) \ {p} ) by BORSUK_1:def 7;

then ([#] (T_1-reflex T)) \ {p} is open by A8;

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

end;reconsider I = (Intersection (Closed_Partitions T)) \ {p} as Subset of (Intersection (Closed_Partitions T)) by XBOOLE_1:36;

A1: the carrier of (T_1-reflex T) = Intersection (Closed_Partitions T) by BORSUK_1:def 7;

then consider x being Element of T such that

A2: p = EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:42;

reconsider q = p as Subset of T by A2;

A3: { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } c= bool the carrier of T

proof

not { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } is empty
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } or Z in bool the carrier of T )

assume Z in { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } ; :: thesis: Z in bool the carrier of T

then ex Y being a_partition of the carrier of T st

( Z = EqClass (x,Y) & Y in Closed_Partitions T ) ;

hence Z in bool the carrier of T ; :: thesis: verum

end;assume Z in { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } ; :: thesis: Z in bool the carrier of T

then ex Y being a_partition of the carrier of T st

( Z = EqClass (x,Y) & Y in Closed_Partitions T ) ;

hence Z in bool the carrier of T ; :: thesis: verum

proof

then reconsider m = { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } as non empty Subset-Family of T by A3;
consider Y being object such that

A4: Y in Closed_Partitions T by XBOOLE_0:def 1;

reconsider Y = Y as a_partition of the carrier of T by A4, EQREL_1:def 7;

EqClass (x,Y) in { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } by A4;

hence not { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } is empty ; :: thesis: verum

end;A4: Y in Closed_Partitions T by XBOOLE_0:def 1;

reconsider Y = Y as a_partition of the carrier of T by A4, EQREL_1:def 7;

EqClass (x,Y) in { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } by A4;

hence not { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } is empty ; :: thesis: verum

reconsider m = m as non empty Subset-Family of T ;

A5: for A being Subset of T st A in m holds

A is closed

proof

p = meet { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T }
by A2, EQREL_1:def 8;
let A be Subset of T; :: thesis: ( A in m implies A is closed )

assume A in m ; :: thesis: A is closed

then consider S being a_partition of the carrier of T such that

A6: ( A = EqClass (x,S) & S in Closed_Partitions T ) ;

( ex B being a_partition of the carrier of T st

( S = B & B is closed ) & A in S ) by A6, EQREL_1:def 6;

hence A is closed by TOPS_2:def 2; :: thesis: verum

end;assume A in m ; :: thesis: A is closed

then consider S being a_partition of the carrier of T such that

A6: ( A = EqClass (x,S) & S in Closed_Partitions T ) ;

( ex B being a_partition of the carrier of T st

( S = B & B is closed ) & A in S ) by A6, EQREL_1:def 6;

hence A is closed by TOPS_2:def 2; :: thesis: verum

then q is closed by A5, PRE_TOPC:14;

then ([#] T) \ q is open ;

then A7: ([#] T) \ p in the topology of T ;

p in Intersection (Closed_Partitions T) by A1;

then union ((Intersection (Closed_Partitions T)) \ {p}) in the topology of T by A7, EQREL_1:44;

then A8: I in { A where A is Subset of (Intersection (Closed_Partitions T)) : union A in the topology of T } ;

reconsider I = I as Subset of (space (Intersection (Closed_Partitions T))) by BORSUK_1:def 7;

reconsider I = I as Subset of (T_1-reflex T) ;

( the topology of (space (Intersection (Closed_Partitions T))) = { A where A is Subset of (Intersection (Closed_Partitions T)) : union A in the topology of T } & I = ([#] (T_1-reflex T)) \ {p} ) by BORSUK_1:def 7;

then ([#] (T_1-reflex T)) \ {p} is open by A8;

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