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

A5: now :: thesis: not g2 < g1

assume g2 < g1 ; :: thesis: contradiction
then ex r1 being Real st
( r1 in X & r1 < g2 + (g1 - g2) ) by A4, XREAL_1:50;
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: not g1 < g2

assume g1 < g2 ; :: thesis: contradiction
then ex r1 being Real st
( r1 in X & r1 < g1 + (g2 - g1) ) by A2, XREAL_1:50;
hence contradiction by A3; :: thesis: verum

end;

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