let g1, g2 be real number ; :: thesis: for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) holds
g1 = g2
let X be real-membered set ; :: thesis: ( ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) implies g1 = g2 )
assume that
A1: for r being real number st r in X holds
r <= g1 and
A2: for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) and
A3: for r being real number st r in X holds
r <= g2 and
A4: for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ; :: thesis: g1 = g2

A5: now

assume g1 < g2 ; :: thesis: contradiction
then consider r1 being real number such that
A6: r1 in X and
A7: g2 - (g2 - g1) < r1 by A4, XREAL_1:52;
thus contradiction by A1, A6, A7; :: thesis: verum

end;

now

assume g2 < g1 ; :: thesis: contradiction
then consider r1 being real number such that
A8: r1 in X and
A9: g1 - (g1 - g2) < r1 by A2, XREAL_1:52;
thus contradiction by A3, A8, A9; :: thesis: verum

end;

hence g1 = g2 by A5, XXREAL_0:1; :: thesis: verum