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