for Gi being non trivial finite Subset of REAL
for xi being Real st xi in Gi holds
ex ri being Element of REAL st [xi,ri] is Gap of Gi