let A be non empty Interval; :: thesis: for b being ExtReal st ex a being ExtReal st
( a <= b & A = [.a,b.[ ) holds
b = sup A
let IT be ExtReal; :: thesis: ( ex a being ExtReal st
( a <= IT & A = [.a,IT.[ ) implies IT = sup A )
given a being ExtReal such that A1: a <= IT and
A2: A = [.a,IT.[ ; :: thesis: IT = sup A
a <> IT by A2;
then a < IT by A1, XXREAL_0:1;
hence IT = sup A by A2, XXREAL_2:31; :: thesis: verum