let g1, g2 be Real; 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 ; ( ( 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 )
; g1 = g2
A5:
now not g2 < g1assume
g2 < g1
;
contradictionthen
ex
r1 being
Real st
(
r1 in X &
g1 - (g1 - g2) < r1 )
by A2, XREAL_1:50;
hence
contradiction
by A3;
verum end;
now not g1 < g2assume
g1 < g2
;
contradictionthen
ex
r1 being
Real st
(
r1 in X &
g2 - (g2 - g1) < r1 )
by A4, XREAL_1:50;
hence
contradiction
by A1;
verum end;
hence
g1 = g2
by A5, XXREAL_0:1; verum