let Y be non trivial T_0-TopSpace; :: thesis: ( not Y is T_1 implies Sierpinski_Space is_Retract_of Y )

given p, q being Point of Y such that A1: p <> q and

A2: for W, V being Subset of Y st W is open & V is open & p in W & not q in W & q in V holds

p in V ; :: according to URYSOHN1:def 7 :: thesis: Sierpinski_Space is_Retract_of Y

( ex V being Subset of Y st

( V is open & p in V & not q in V ) or ex W being Subset of Y st

( W is open & not p in W & q in W ) ) by A1, TSP_1:def 3;

then consider V being Subset of Y such that

A3: V is open and

A4: ( ( p in V & not q in V ) or ( not p in V & q in V ) ) ;

A5: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def 2;

then consider x, y being Element of (Omega Y) such that

A6: ( ( p in V & not q in V & x = q & y = p ) or ( not p in V & q in V & x = p & y = q ) ) by A4;

then reconsider i = (0,1) --> (x,y) as continuous Function of Sierpinski_Space,Y by A5, YELLOW12:36;

reconsider V = V as open Subset of (Omega Y) by A3, A5, TOPS_3:76;

reconsider c = chi (V, the carrier of Y) as continuous Function of Y,Sierpinski_Space by A3, YELLOW16:46;

c * i = id Sierpinski_Space by A5, A6, YELLOW16:48;

hence Sierpinski_Space is_Retract_of Y by WAYBEL25:def 1; :: thesis: verum

given p, q being Point of Y such that A1: p <> q and

A2: for W, V being Subset of Y st W is open & V is open & p in W & not q in W & q in V holds

p in V ; :: according to URYSOHN1:def 7 :: thesis: Sierpinski_Space is_Retract_of Y

( ex V being Subset of Y st

( V is open & p in V & not q in V ) or ex W being Subset of Y st

( W is open & not p in W & q in W ) ) by A1, TSP_1:def 3;

then consider V being Subset of Y such that

A3: V is open and

A4: ( ( p in V & not q in V ) or ( not p in V & q in V ) ) ;

A5: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def 2;

then consider x, y being Element of (Omega Y) such that

A6: ( ( p in V & not q in V & x = q & y = p ) or ( not p in V & q in V & x = p & y = q ) ) by A4;

now :: thesis: for W being open Subset of (Omega Y) st x in W holds

y in W

then
(0,1) --> (x,y) is continuous Function of Sierpinski_Space,(Omega Y)
by YELLOW16:47;y in W

let W be open Subset of (Omega Y); :: thesis: ( x in W implies y in W )

W is open Subset of Y by A5, TOPS_3:76;

hence ( x in W implies y in W ) by A2, A3, A6; :: thesis: verum

end;W is open Subset of Y by A5, TOPS_3:76;

hence ( x in W implies y in W ) by A2, A3, A6; :: thesis: verum

then reconsider i = (0,1) --> (x,y) as continuous Function of Sierpinski_Space,Y by A5, YELLOW12:36;

reconsider V = V as open Subset of (Omega Y) by A3, A5, TOPS_3:76;

reconsider c = chi (V, the carrier of Y) as continuous Function of Y,Sierpinski_Space by A3, YELLOW16:46;

c * i = id Sierpinski_Space by A5, A6, YELLOW16:48;

hence Sierpinski_Space is_Retract_of Y by WAYBEL25:def 1; :: thesis: verum