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 A2: [li',ri'] is Gap of Gi ; :: thesis: ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) )
then A3: li' in Gi by Th17;
A4: ri' in Gi by A2, Th17;
A5: ( li' = li or li' = ri ) by A1, A3, TARSKI:def 2;
li' <> ri' by A2, Th17;
hence ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = 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 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 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 ( ( ( li' = li & ri' = ri ) or ( li' = ri & ri' = li ) ) implies [li',ri'] is Gap of Gi ) by A1; :: thesis: verum