let Gi be non trivial finite Subset of REAL ; :: thesis: for li, ri, li', ri' being Real st Gi = {li,ri} holds
( [li',ri'] is Gap of Gi iff ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) ) )
let li, ri, li', ri' be Real; :: thesis: ( Gi = {li,ri} implies ( [li',ri'] is Gap of Gi iff ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) ) ) )
assume A1: Gi = {li,ri} ; :: thesis: ( [li',ri'] is Gap of Gi iff ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) ) )

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

assume [li',ri'] is Gap of Gi ; :: thesis: ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) )
then ( li' in Gi & ri' in Gi & li' <> ri' ) by Th17;
then ( ( li' = li or li' = ri ) & ( ri' = li or ri' = ri ) & li' <> ri' ) by A1, TARSKI:def 2;
hence ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) ) ; :: 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 A2: Gi = {li,ri} ; :: thesis: [li,ri] is Gap of Gi
take li ; :: according to CHAIN_1:def 6 :: 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 A2, 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 A2, 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 A2, TARSKI:def 2, XXREAL_0:1; :: thesis: verum

end;

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