let X be non empty ext-real-membered set ; :: thesis: ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) )
for y being ExtReal st y in SetMajorant X holds
sup X <= y

proof

let y be ExtReal; :: thesis: ( y in SetMajorant X implies sup X <= y )
assume y in SetMajorant X ; :: thesis: sup X <= y
then y is UpperBound of X by Def1;
hence sup X <= y by XXREAL_2:def 3; :: thesis: verum

end;

then A1: sup X is LowerBound of SetMajorant X by XXREAL_2:def 2;
inf X is LowerBound of X by XXREAL_2:def 4;
then A2: inf X in SetMinorant X by Def2;
for y being ExtReal st y in SetMinorant X holds
y <= inf X

proof

let y be ExtReal; :: thesis: ( y in SetMinorant X implies y <= inf X )
assume y in SetMinorant X ; :: thesis: y <= inf X
then y is LowerBound of X by Def2;
hence y <= inf X by XXREAL_2:def 4; :: thesis: verum

end;

then A3: inf X is UpperBound of SetMinorant X by XXREAL_2:def 1;
sup X is UpperBound of X by XXREAL_2:def 3;
then sup X in SetMajorant X by Def1;
hence ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) ) by A1, A2, A3, XXREAL_2:55, XXREAL_2:56; :: thesis: verum