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
let 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
proof
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;
not { (EqClass (x,S)) where S is a_partition of the carrier of T : S in Closed_Partitions T } is empty
proof
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;
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;
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
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;
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;
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;
hence T_1-reflex T is T_1 by URYSOHN1:19; :: thesis: verum