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

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

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

for y being ExtReal st y in SetMajorant X holds

sup X <= y

proof

then A1:
sup X is LowerBound of SetMajorant X
by XXREAL_2:def 2;
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;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

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

then A3:
inf X is UpperBound of SetMinorant X
by XXREAL_2:def 1;
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;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

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