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 li9, ri9 being Real such that
A1: [li,ri] = [li9,ri9] and
A2: li9 in Gi and
A3: ri9 in Gi and
A4: ( ( li9 < ri9 & ( for xi being Real st xi in Gi & li9 < xi holds
not xi < ri9 ) ) or ( ri9 < li9 & ( for xi being Real st xi in Gi holds
( not li9 < xi & not xi < ri9 ) ) ) ) by Def5;
A5: li9 = li by A1, XTUPLE_0:1;
ri9 = ri by A1, XTUPLE_0:1;
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; :: thesis: verum
end;
( li in REAL & ri in REAL ) by XREAL_0:def 1;
then [li,ri] in [:REAL,REAL:] by ZFMISC_1:87;
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 ) ) ) ) implies [li,ri] is Gap of Gi ) by Def5; :: thesis: verum