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 ) )
assume S = Rainbow p,G ; :: thesis: for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
then A1: S c= DYADIC by Th15;
let e1 be R_eal; :: thesis: ( e1 = 1 implies ( 0. <= sup S & sup S <= e1 ) )
assume A2: e1 = 1 ; :: thesis: ( 0. <= sup S & sup S <= e1 )
reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def 1;
A3: S c= [.a,b.] by A1, URYSOHN2:32, XBOOLE_1:1;
then for x being ext-real number st x in S holds
x <= e1 by A2, XXREAL_1:1;
then A4: e1 is UpperBound of S by XXREAL_2:def 1;
consider s being set such that
A5: s in S by XBOOLE_0:def 1;
reconsider s = s as R_eal by A5;
( 0. <= s & s <= sup S ) by A3, A5, XXREAL_1:1, XXREAL_2:4;
hence ( 0. <= sup S & sup S <= e1 ) by A4, XXREAL_2:def 3; :: thesis: verum