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