let T be non empty TopSpace; :: thesis: for x, y being Element of T st ( for W being open Subset of T st y in W holds
x in W ) holds
(0,1) --> (y,x) is continuous Function of Sierpinski_Space,T
let x, y be Element of T; :: thesis: ( ( for W being open Subset of T st y in W holds
x in W ) implies (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T )
assume A1: for W being open Subset of T st y in W holds
x in W ; :: thesis: (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T
A2: the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then reconsider i = (0,1) --> (y,x) as Function of Sierpinski_Space,T ;
A3: i . 1 = x by FUNCT_4:63;
A4: not 1 in {0} by TARSKI:def 1;
A5: 0 in {0} by TARSKI:def 1;
A6: 1 in {0,1} by TARSKI:def 2;
A7: i . 0 = y by FUNCT_4:63;

A8: now

let W be Subset of T; :: thesis: ( W is open implies i " W is open )
assume W is open ; :: thesis: i " W is open
then A9: ( ( y in W & x in W ) or ( not y in W & x in W ) or ( not y in W & not x in W ) ) by A1;
( i " W = {} or i " W = {0} or i " W = {1} or i " W = {0,1} ) by A2, ZFMISC_1:36;
then i " W in {{},{1},{0,1}} by A7, A3, A6, A5, A4, A9, ENUMSET1:def 1, FUNCT_2:38;
then i " W in the topology of Sierpinski_Space by WAYBEL18:def 9;
hence i " W is open by PRE_TOPC:def 2; :: thesis: verum

end;

[#] T <> {} ;
hence (0,1) --> (y,x) is continuous Function of Sierpinski_Space,T by A8, TOPS_2:43; :: thesis: verum