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

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

assume A1: x <= y ; :: thesis: sup [.x,y.] = y

A2: for z being UpperBound of [.x,y.] holds y <= z

proof

y is UpperBound of [.x,y.]
by Th21;
let z be UpperBound of [.x,y.]; :: thesis: y <= z

y in [.x,y.] by A1, XXREAL_1:1;

hence y <= z by Def1; :: thesis: verum

end;y in [.x,y.] by A1, XXREAL_1:1;

hence y <= z by Def1; :: thesis: verum

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