for p being Real
for X being Subset of REAL st 0 < p & ex r being Real st r in X & ( for r being Real st r in X holds
r + p in X ) holds
for g being Real ex r being Real st
( r in X & g < r )