:: deftheorem Def5 defines Gap CHAIN_1:def 5 :
for Gi being non trivial finite Subset of REAL
for b₂ being Element of [:REAL,REAL:] holds
( b₂ is Gap of Gi iff ex li, ri being Real st
( b₂ = [li,ri] & 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 ) ) ) ) ) );