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 )
reconsider B = [.a,b.] as non empty Subset of ExtREAL by A1, MEMBERED:2;
A3: a <= inf A

proof

for x being ext-real number 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 by XXREAL_2:def 4; :: thesis: verum

end;

sup A <= b

proof

for x being ext-real number st x in B holds
x <= b by XXREAL_1:1;
then b is UpperBound of B by XXREAL_2:def 1;
then b is UpperBound of A by A1, XXREAL_2:6;
hence sup A <= b by XXREAL_2:def 3; :: thesis: verum

end;

hence ( a <= inf A & sup A <= b ) by A3; :: thesis: verum