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_{1}[ 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_{1}[x,y]

for x being Element of DOM holds S_{1}[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_{1}[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

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

$2 = (G . n) . $1 ) );

A2: for x being Element of DOM ex y being Subset of T st S

proof

ex F being Function of DOM,(bool the carrier of T) st
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_{1}[x,y]

A3: ( x in (halfline 0) \/ DYADIC or x in right_open_halfline 1 ) by URYSOHN1:def 3, XBOOLE_0:def 3;

end;let x be Element of DOM ; :: thesis: ex y being Subset of T st S

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;

end;

suppose A4:
x in halfline 0
; :: thesis: ex y being Subset of T st S_{1}[x,y]

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

s = s ;

hence ex y being Subset of T st S_{1}[x,y]
by A5; :: thesis: verum

end;proof

reconsider s = {} as Subset of T by XBOOLE_1:2;
assume A6:
( x in right_open_halfline 1 or x in DYADIC )
; :: thesis: contradiction

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

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;a <= x by A7, URYSOHN2:28, XXREAL_1:1;

hence contradiction by A4, XXREAL_1:233; :: thesis: verum

s = s ;

hence ex y being Subset of T st S

suppose A8:
x in DYADIC
; :: thesis: ex y being Subset of T st S_{1}[x,y]

A9:
not x in halfline 0

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_{1}[x,y]
by A11, A9; :: thesis: verum

end;proof

A11:
not x in right_open_halfline 1
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;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

proof

ex s being Subset of T st
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;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

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

suppose A13:
x in right_open_halfline 1
; :: thesis: ex y being Subset of T st S_{1}[x,y]

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

then reconsider s = the carrier of T as Subset of T ;

s = s ;

hence ex y being Subset of T st S_{1}[x,y]
by A14; :: thesis: verum

end;proof

the carrier of T c= the carrier of T
;
assume A15:
( x in halfline 0 or x in DYADIC )
; :: thesis: contradiction

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

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;x <= b by A16, URYSOHN2:28, XXREAL_1:1;

hence contradiction by A13, XXREAL_1:235; :: thesis: verum

then reconsider s = the carrier of T as Subset of T ;

s = s ;

hence ex y being Subset of T st S

for x being Element of DOM holds S

then consider F being Function of DOM,(bool the carrier of T) such that

A17: for x being Element of DOM holds S

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