theorem Th16: :: CHAIN_1:19

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