theorem Th17: :: CHAIN_1:20
for Gi being non trivial finite Subset of REAL
for li, ri, ri9 being Real st [li,ri] is Gap of Gi & [li,ri9] is Gap of Gi holds
ri = ri9