let x, y be ext-real number ; :: thesis: ( x <= y implies sup [.x,y.] = y )
A: y is UpperBound of [.x,y.] by Th21;
assume Z: x <= y ; :: thesis: sup [.x,y.] = y
for z being UpperBound of [.x,y.] holds y <= z

proof

let z be UpperBound of [.x,y.]; :: thesis: y <= z
y in [.x,y.] by Z, XXREAL_1:1;
hence y <= z by Def1; :: thesis: verum

end;

hence sup [.x,y.] = y by A, Def3; :: thesis: verum