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 Th17;
A4: ri9 in Gi by A2, Th17;
A5: ( li9 = li or li9 = ri ) by A1, A3, TARSKI:def 2;
li9 <> ri9 by A2, Th17;
hence ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) by A1, A4, A5, TARSKI:def 2; :: thesis: verum

end;

for Gi being non trivial finite Subset of REAL
for li, ri being Real st Gi = {li,ri} holds
[li,ri] is Gap of Gi

proof

let Gi be non trivial finite Subset of REAL; :: thesis: for li, ri being Real st Gi = {li,ri} holds
[li,ri] is Gap of Gi
let li, ri be Real; :: thesis: ( Gi = {li,ri} implies [li,ri] is Gap of Gi )
assume A6: Gi = {li,ri} ; :: thesis: [li,ri] is Gap of Gi
take li ; :: according to CHAIN_1:def 5 :: thesis: ex ri being Real st
( [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 ) ) ) ) )
take ri ; :: thesis: ( [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 ) ) ) ) )
thus ( [li,ri] = [li,ri] & li in Gi & ri in Gi ) by A6, TARSKI:def 2; :: thesis: ( ( 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 <> ri by A6, Th4;
hence ( ( 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 A6, TARSKI:def 2, XXREAL_0:1; :: thesis: verum

end;

hence ( ( ( li9 = li & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) implies [li9,ri9] is Gap of Gi ) by A1; :: thesis: verum