let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B ex F being Function of DOM ,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B ex F being Function of DOM ,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) ) )
assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B ex F being Function of DOM ,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
let G be Rain of A,B; :: thesis: ex F being Function of DOM ,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
defpred S₁[ Element of DOM , set ] means ( ( $1 in halfline 0 implies $2 = {} ) & ( $1 in right_open_halfline 1 implies $2 = the carrier of T ) & ( $1 in DYADIC implies for n being Element of NAT st $1 in dyadic n holds
$2 = (G . n) . $1 ) );
A2: for x being Element of DOM ex y being Subset of T st S₁[x,y]

proof

let x be Element of DOM ; :: thesis: ex y being Subset of T st S₁[x,y]
A3: ( x in (halfline 0 ) \/ DYADIC or x in right_open_halfline 1 ) by URYSOHN1:def 5, XBOOLE_0:def 3;
reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def 1;

per cases ( x in halfline 0 or x in DYADIC or x in right_open_halfline 1 ) by A3, XBOOLE_0:def 3;

suppose A5: x in halfline 0 ; :: thesis: ex y being Subset of T st S₁[x,y]

reconsider s = {} as Subset of T by XBOOLE_1:2;
A6: s = s ;
( not x in right_open_halfline 1 & not x in DYADIC )

proof

assume A7: ( x in right_open_halfline 1 or x in DYADIC ) ; :: thesis: contradiction

per cases ( x in right_open_halfline 1 or x in DYADIC ) by A7;

suppose x in right_open_halfline 1 ; :: thesis: contradiction

then 1 < x by XXREAL_1:235;
hence contradiction by A5, XXREAL_1:233; :: thesis: verum

end;

suppose A8: x in DYADIC ; :: thesis: contradiction

reconsider x = x as R_eal by XXREAL_0:def 1;
( a <= x & x <= b & x in REAL ) by A8, URYSOHN2:32, XXREAL_1:1;
hence contradiction by A5, XXREAL_1:233; :: thesis: verum

end;

end;

end;

hence ex y being Subset of T st S₁[x,y] by A6; :: thesis: verum

end;

suppose A9: x in DYADIC ; :: thesis: ex y being Subset of T st S₁[x,y]

then consider s being Subset of T such that
A10: for n being Element of NAT st x in dyadic n holds
s = (G . n) . x by A1, Th10;
A11: not x in right_open_halfline 1

proof

assume A12: x in right_open_halfline 1 ; :: thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def 1;
( a <= x & x <= b & x in REAL ) by A9, URYSOHN2:32, XXREAL_1:1;
hence contradiction by A12, XXREAL_1:235; :: thesis: verum

end;

not x in halfline 0

proof

assume A13: x in halfline 0 ; :: thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def 1;
( a <= x & x <= b & x in REAL ) by A9, URYSOHN2:32, XXREAL_1:1;
hence contradiction by A13, XXREAL_1:233; :: thesis: verum

end;

hence ex y being Subset of T st S₁[x,y] by A10, A11; :: thesis: verum

end;

suppose A14: x in right_open_halfline 1 ; :: thesis: ex y being Subset of T st S₁[x,y]

the carrier of T c= the carrier of T ;
then reconsider s = the carrier of T as Subset of T ;
A15: s = s ;
( not x in halfline 0 & not x in DYADIC )

proof

assume A16: ( x in halfline 0 or x in DYADIC ) ; :: thesis: contradiction

per cases ( x in halfline 0 or x in DYADIC ) by A16;

suppose x in halfline 0 ; :: thesis: contradiction

then x < 0 by XXREAL_1:233;
hence contradiction by A14, XXREAL_1:235; :: thesis: verum

end;

suppose A17: x in DYADIC ; :: thesis: contradiction

reconsider x = x as R_eal by XXREAL_0:def 1;
( a <= x & x <= b & x in REAL ) by A17, URYSOHN2:32, XXREAL_1:1;
hence contradiction by A14, XXREAL_1:235; :: thesis: verum

end;

end;

end;

hence ex y being Subset of T st S₁[x,y] by A15; :: thesis: verum

end;

end;

end;

ex F being Function of DOM ,(bool the carrier of T) st
for x being Element of DOM holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
then consider F being Function of DOM ,(bool the carrier of T) such that
A18: for x being Element of DOM holds S₁[x,F . x] ;
take F ; :: thesis: for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
thus for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) ) by A18; :: thesis: verum