let x, y be ext-real number ; :: thesis: ( x < y implies sup ].x,y.[ = y )
A: y is UpperBound of ].x,y.[ by Th24;
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
for r being ext-real number st x < r & r < y holds
r <= z

proof

let r be ext-real number ; :: thesis: ( x < r & r < y implies r <= z )
assume ( x < r & r < y ) ; :: thesis: r <= z
then r in ].x,y.[ by XXREAL_1:4;
hence r <= z by Def1; :: thesis: verum

end;

hence y <= z by Z, XREAL_1:231; :: thesis: verum

end;

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