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 9 :: 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;
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:48;
then
0 ,1 --> x,y is continuous Function of Sierpinski_Space ,(Omega Y)
by YELLOW16:49;
then reconsider i = 0 ,1 --> x,y as continuous Function of Sierpinski_Space ,Y by A5, YELLOW12:36;
c * i = id Sierpinski_Space
by A5, A6, YELLOW16:50;
hence
Sierpinski_Space is_Retract_of Y
by WAYBEL25:def 1; :: thesis: verum