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

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

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

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

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: