let A be non empty Subset of ExtREAL; :: thesis: for a, b being R_eal st A c= [.a,b.] holds
( a <= inf A & sup A <= b )
let a, b be R_eal; :: thesis: ( A c= [.a,b.] implies ( a <= inf A & sup A <= b ) )
assume A1: A c= [.a,b.] ; :: thesis: ( a <= inf A & sup A <= b )
then reconsider B = [.a,b.] as non empty Subset of ExtREAL by MEMBERED:2;
for x being ExtReal st x in B holds
x <= b by XXREAL_1:1;
then b is UpperBound of B by XXREAL_2:def 1;
then A2: b is UpperBound of A by A1, XXREAL_2:6;
for x being ExtReal st x in B holds
a <= x by XXREAL_1:1;
then a is LowerBound of B by XXREAL_2:def 2;
then a is LowerBound of A by A1, XXREAL_2:5;
hence ( a <= inf A & sup A <= b ) by A2, XXREAL_2:def 3, XXREAL_2:def 4; :: thesis: verum