let x, y be ExtReal; :: thesis: ( x < y implies sup ].x,y.[ = y )
assume A1: x < y ; :: thesis: sup ].x,y.[ = y
A2: for z being UpperBound of ].x,y.[ holds y <= z

proof

let z be UpperBound of ].x,y.[; :: thesis: y <= z
for r being ExtReal st x < r & r < y holds
r <= z by XXREAL_1:4, Def1;
hence y <= z by A1, XREAL_1:229; :: thesis: verum

end;

y is UpperBound of ].x,y.[ by Th24;
hence sup ].x,y.[ = y by A2, Def3; :: thesis: verum