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 Th23;
let z be UpperBound of [.x,y.[; :: thesis: y <= z

for r being ExtReal st x < r & r < y holds

r <= z

end;for r being ExtReal st x < r & r < y holds

r <= z

proof

hence
y <= z
by A1, XREAL_1:229; :: thesis: verum
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;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

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