theorem Th13: :: CHAIN_1:16

for Gi being non trivial finite Subset of REAL
for li, ri being Real holds
( [li,ri] is Gap of Gi iff ( li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) ) )