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 S1[ 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 S1[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 S1[x,y]
A3: ( x in () \/ DYADIC or x in right_open_halfline 1 ) by ;
per cases by ;
suppose A4: x in halfline 0 ; :: thesis: ex y being Subset of T st S1[x,y]
end;
suppose A8: x in DYADIC ; :: thesis: ex y being Subset of T st S1[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 ;
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 ;
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 S1[x,y] by ; :: thesis: verum
end;
suppose A13: x in right_open_halfline 1 ; :: thesis: ex y being Subset of T st S1[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
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 S1[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 S1[x,F . x] from then consider F being Function of DOM,(bool the carrier of T) such that
A17: for x being Element of DOM holds S1[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