theorem Th8: :: SEQ_4:8

for g1, g2 being Real
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