let Gi be non trivial finite Subset of ; 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 ) ) ) ) ) )
let li, ri be Real; ( [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 ) ) ) ) ) )
thus
( [li,ri] is Gap of Gi implies ( 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 ) ) ) ) ) )
( 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 ) ) ) ) implies [li,ri] is Gap of Gi )proof
assume
[li,ri] is
Gap of
Gi
;
( 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 ) ) ) ) )
then consider li',
ri' being
Real such that A1:
[li,ri] = [li',ri']
and A2:
li' in Gi
and A3:
ri' in Gi
and A4:
( (
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' ) ) ) )
by Def6;
A5:
li' = li
by A1, ZFMISC_1:33;
ri' = ri
by A1, ZFMISC_1:33;
hence
(
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 ) ) ) ) )
by A2, A3, A4, A5;
verum
end;
thus
( 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 ) ) ) ) implies [li,ri] is Gap of Gi )
by Def6; verum