let Gi be non trivial finite Subset of REAL ; :: thesis: 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; :: thesis: ( [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 ) ) ) ) ) )
:: thesis: ( 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
;
:: thesis: ( 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'] &
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 Def6;
(
li' = li &
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 A1;
:: thesis: 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; :: thesis: verum