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