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
y in ].x,y.] by A1, XXREAL_1:2;
hence y <= z by Def1; :: thesis: verum

end;

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