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 ) ) )
hereby :: thesis: ( ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) implies [li9,ri9] is Gap of Gi )
assume 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;
assume A6: ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) ; :: thesis: [li9,ri9] is Gap of Gi
( 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
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;
hence [li9,ri9] is Gap of Gi ; :: thesis: verum