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

ri = ri9

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

A1: ( ri <= ri9 & ri9 <= ri implies ri = ri9 ) by XXREAL_0:1;

assume that

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

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

A4: ri in Gi by A2, Th13;

A5: ri9 in Gi by A3, Th13;

ri = ri9

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

A1: ( ri <= ri9 & ri9 <= ri implies ri = ri9 ) by XXREAL_0:1;

assume that

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

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

A4: ri in Gi by A2, Th13;

A5: ri9 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;