theorem Th11: :: CHAIN_1:13

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