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 . 0 = y & i . 1 = x ) by FUNCT_4:66;
A4: ( 0 in {0 ,1} & 1 in {0 ,1} & 0 in {0 } & not 1 in {0 } ) by TARSKI:def 1, TARSKI:def 2;
A5: [#] T <> {} ;

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 A6: ( ( 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 A3, A4, A6, 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;

hence 0 ,1 --> y,x is continuous Function of Sierpinski_Space ,T by A5, TOPS_2:55; :: thesis: verum