reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def 1;

let T be non empty TopSpace; :: thesis: for A, B being Subset of T

for G being Rain of A,B

for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let A, B be Subset of T; :: thesis: for G being Rain of A,B

for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let G be Rain of A,B; :: thesis: for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let p be Point of T; :: thesis: for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let S be non empty Subset of ExtREAL; :: thesis: ( S = Rainbow (p,G) implies for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 ) )

consider s being object such that

A1: s in S by XBOOLE_0:def 1;

reconsider s = s as R_eal by A1;

assume S = Rainbow (p,G) ; :: thesis: for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

then S c= DYADIC by Th13;

then A2: S c= [.a,b.] by URYSOHN2:28;

let e1 be R_eal; :: thesis: ( e1 = 1 implies ( 0. <= sup S & sup S <= e1 ) )

assume e1 = 1 ; :: thesis: ( 0. <= sup S & sup S <= e1 )

then for x being ExtReal st x in S holds

x <= e1 by A2, XXREAL_1:1;

then A3: e1 is UpperBound of S by XXREAL_2:def 1;

0. <= s by A2, A1, XXREAL_1:1;

hence ( 0. <= sup S & sup S <= e1 ) by A3, A1, XXREAL_2:4, XXREAL_2:def 3; :: thesis: verum

let T be non empty TopSpace; :: thesis: for A, B being Subset of T

for G being Rain of A,B

for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let A, B be Subset of T; :: thesis: for G being Rain of A,B

for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let G be Rain of A,B; :: thesis: for p being Point of T

for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let p be Point of T; :: thesis: for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds

for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

let S be non empty Subset of ExtREAL; :: thesis: ( S = Rainbow (p,G) implies for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 ) )

consider s being object such that

A1: s in S by XBOOLE_0:def 1;

reconsider s = s as R_eal by A1;

assume S = Rainbow (p,G) ; :: thesis: for e1 being R_eal st e1 = 1 holds

( 0. <= sup S & sup S <= e1 )

then S c= DYADIC by Th13;

then A2: S c= [.a,b.] by URYSOHN2:28;

let e1 be R_eal; :: thesis: ( e1 = 1 implies ( 0. <= sup S & sup S <= e1 ) )

assume e1 = 1 ; :: thesis: ( 0. <= sup S & sup S <= e1 )

then for x being ExtReal st x in S holds

x <= e1 by A2, XXREAL_1:1;

then A3: e1 is UpperBound of S by XXREAL_2:def 1;

0. <= s by A2, A1, XXREAL_1:1;

hence ( 0. <= sup S & sup S <= e1 ) by A3, A1, XXREAL_2:4, XXREAL_2:def 3; :: thesis: verum