let Gi be non trivial finite Subset of REAL; :: thesis: for li, ri, li9, ri9 being Real st Gi = {li,ri} holds

( [li9,ri9] is Gap of Gi iff ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) )

let li, ri, li9, ri9 be Real; :: thesis: ( Gi = {li,ri} implies ( [li9,ri9] is Gap of Gi iff ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) ) )

assume A1: Gi = {li,ri} ; :: thesis: ( [li9,ri9] is Gap of Gi iff ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) )

( li9 in REAL & ri9 in REAL ) by XREAL_0:def 1;

then [li9,ri9] in [:REAL,REAL:] by ZFMISC_1:87;

then reconsider liri = [li9,ri9] as Element of [:REAL,REAL:] ;

liri is Gap of Gi

( [li9,ri9] is Gap of Gi iff ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) )

let li, ri, li9, ri9 be Real; :: thesis: ( Gi = {li,ri} implies ( [li9,ri9] is Gap of Gi iff ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) ) )

assume A1: Gi = {li,ri} ; :: thesis: ( [li9,ri9] is Gap of Gi iff ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) )

hereby :: thesis: ( ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) implies [li9,ri9] is Gap of Gi )

assume A6:
( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) )
; :: thesis: [li9,ri9] is Gap of Giassume A2:
[li9,ri9] is Gap of Gi
; :: thesis: ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) )

then A3: li9 in Gi by Th13;

A4: ri9 in Gi by A2, Th13;

A5: ( li9 = li or li9 = ri ) by A1, A3, TARSKI:def 2;

li9 <> ri9 by A2, Th13;

hence ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) by A1, A4, A5, TARSKI:def 2; :: thesis: verum

end;then A3: li9 in Gi by Th13;

A4: ri9 in Gi by A2, Th13;

A5: ( li9 = li or li9 = ri ) by A1, A3, TARSKI:def 2;

li9 <> ri9 by A2, Th13;

hence ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) by A1, A4, A5, TARSKI:def 2; :: thesis: verum

( li9 in REAL & ri9 in REAL ) by XREAL_0:def 1;

then [li9,ri9] in [:REAL,REAL:] by ZFMISC_1:87;

then reconsider liri = [li9,ri9] as Element of [:REAL,REAL:] ;

liri is Gap of Gi

proof

hence
[li9,ri9] is Gap of Gi
; :: thesis: verum
take
li9
; :: according to CHAIN_1:def 5 :: thesis: ex ri being Real st

( liri = [li9,ri] & li9 in Gi & ri in Gi & ( ( li9 < ri & ( for xi being Real st xi in Gi & li9 < xi holds

not xi < ri ) ) or ( ri < li9 & ( for xi being Real st xi in Gi holds

( not li9 < xi & not xi < ri ) ) ) ) )

take ri9 ; :: thesis: ( liri = [li9,ri9] & li9 in Gi & ri9 in Gi & ( ( 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 ) ) ) ) )

li <> ri by A1, Th3;

hence ( liri = [li9,ri9] & li9 in Gi & ri9 in Gi & ( ( 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 A1, TARSKI:def 2, XXREAL_0:1, A6; :: thesis: verum

end;( liri = [li9,ri] & li9 in Gi & ri in Gi & ( ( li9 < ri & ( for xi being Real st xi in Gi & li9 < xi holds

not xi < ri ) ) or ( ri < li9 & ( for xi being Real st xi in Gi holds

( not li9 < xi & not xi < ri ) ) ) ) )

take ri9 ; :: thesis: ( liri = [li9,ri9] & li9 in Gi & ri9 in Gi & ( ( 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 ) ) ) ) )

li <> ri by A1, Th3;

hence ( liri = [li9,ri9] & li9 in Gi & ri9 in Gi & ( ( 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 A1, TARSKI:def 2, XXREAL_0:1, A6; :: thesis: verum