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 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 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 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 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 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

reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def 1;
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 3, XBOOLE_0:def 3;

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

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

A5: ( not x in right_open_halfline 1 & not x in DYADIC )

proof

assume A6: ( 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 A6;

suppose x in right_open_halfline 1 ; :: thesis: contradiction

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

end;

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

reconsider x = x as R_eal by XXREAL_0:def 1;
a <= x by A7, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A4, XXREAL_1:233; :: thesis: verum

end;

end;

end;

reconsider s = {} as Subset of T by XBOOLE_1:2;
s = s ;
hence ex y being Subset of T st S₁[x,y] by A5; :: thesis: verum

end;

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

A9: not x in halfline 0

proof

assume A10: x in halfline 0 ; :: thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def 1;
a <= x by A8, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A10, XXREAL_1:233; :: thesis: verum

end;

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;
x <= b by A8, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A12, XXREAL_1:235; :: thesis: verum

end;

ex s being Subset of T st
for n being Nat st x in dyadic n holds
s = (G . n) . x by A1, A8, Th9;
hence ex y being Subset of T st S₁[x,y] by A11, A9; :: thesis: verum

end;

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

A14: ( not x in halfline 0 & not x in DYADIC )

proof

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

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

suppose x in halfline 0 ; :: thesis: contradiction

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

end;

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

reconsider x = x as R_eal by XXREAL_0:def 1;
x <= b by A16, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A13, XXREAL_1:235; :: thesis: verum

end;

end;

end;

the carrier of T c= the carrier of T ;
then reconsider s = the carrier of T as Subset of T ;
s = s ;
hence ex y being Subset of T st S₁[x,y] by A14; :: 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
A17: 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 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 Nat st x in dyadic n holds
F . x = (G . n) . x ) ) by A17; :: thesis: verum