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

proof

let r be ExtReal; :: thesis: ( x < r & r < y implies r <= z )
assume that
A3: x < r and
A4: r < y ; :: thesis: r <= z
r in [.x,y.[ by A3, A4, XXREAL_1:3;
hence r <= z by Def1; :: thesis: verum

end;

hence y <= z by A1, XREAL_1:229; :: thesis: verum

end;

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