theorem :: CHAIN_1:15

for Gi being non trivial finite Subset of REAL ex li, ri being Real st
( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds
( not xi < ri & not li < xi ) ) )