let g1, g2 be Real; :: thesis: for X being real-membered set st ( for r being Real st r in X holds
r <= g1 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g1 - s < r ) ) & ( for r being Real st r in X holds
r <= g2 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g2 - s < r ) ) holds
g1 = g2
let X be real-membered set ; :: thesis: ( ( for r being Real st r in X holds
r <= g1 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g1 - s < r ) ) & ( for r being Real st r in X holds
r <= g2 ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & g2 - s < r ) ) implies g1 = g2 )
assume that
A1: for r being Real st r in X holds
r <= g1 and
A2: for s being Real st 0 < s holds
ex r being Real st
( r in X & g1 - s < r ) and
A3: for r being Real st r in X holds
r <= g2 and
A4: for s being Real st 0 < s holds
ex r being Real st
( r in X & g2 - s < r ) ; :: thesis: g1 = g2
A5: now :: thesis: not g2 < g1
assume g2 < g1 ; :: thesis: contradiction
then ex r1 being Real st
( r1 in X & g1 - (g1 - g2) < r1 ) by A2, XREAL_1:50;
hence contradiction by A3; :: thesis: verum
end;
now :: thesis: not g1 < g2
assume g1 < g2 ; :: thesis: contradiction
then ex r1 being Real st
( r1 in X & g2 - (g2 - g1) < r1 ) by A4, XREAL_1:50;
hence contradiction by A1; :: thesis: verum
end;
hence g1 = g2 by A5, XXREAL_0:1; :: thesis: verum