let Gi be non trivial finite Subset of REAL; :: thesis: for li, ri, li9 being Real st [li,ri] is Gap of Gi & [li9,ri] is Gap of Gi holds

li = li9

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

A1: ( li <= li9 & li9 <= li implies li = li9 ) by XXREAL_0:1;

assume that

A2: [li,ri] is Gap of Gi and

A3: [li9,ri] is Gap of Gi ; :: thesis: li = li9

A4: li in Gi by A2, Th13;

A5: li9 in Gi by A3, Th13;

li = li9

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

A1: ( li <= li9 & li9 <= li implies li = li9 ) by XXREAL_0:1;

assume that

A2: [li,ri] is Gap of Gi and

A3: [li9,ri] is Gap of Gi ; :: thesis: li = li9

A4: li in Gi by A2, Th13;

A5: li9 in Gi by A3, Th13;

per cases
( ( 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, Th13;

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

( not li < xi & not xi < ri ) ) ) ) by A2, Th13;

end;