let A be non empty Interval; :: thesis: for b being R_eal st ex a being R_eal st
( a <= b & A = ].a,b.] ) holds
b = sup A
let IT be R_eal; :: thesis: ( ex a being R_eal st
( a <= IT & A = ].a,IT.] ) implies IT = sup A )
given a being R_eal such that G1: a <= IT and
G2: A = ].a,IT.] ; :: thesis: IT = sup A
a <> IT by G2;
then a < IT by G1, XXREAL_0:1;
hence IT = sup A by G2, XXREAL_2:30; :: thesis: verum