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:66;
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:66;

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:42;
then i " W in {{} ,{1},{0 ,1}} by A7, A3, A6, A5, A4, A9, ENUMSET1:def 1, FUNCT_2:46;
then i " W in the topology of Sierpinski_Space by WAYBEL18:def 9;
hence i " W is open by PRE_TOPC:def 5; :: thesis: verum

end;

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