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;

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;

suppose A6: ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) ; :: thesis: ri = ri9

( ri9 <= li or ( li < ri9 & ri9 < ri ) or ri <= ri9 ) ;
hence ri = ri9 by A1, A3, A4, A5, A6, Th13; :: thesis: verum

end;

suppose A7: ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ; :: thesis: ri = ri9

( ri9 < ri or ( ri <= ri9 & ri9 <= li ) or li < ri9 ) ;
hence ri = ri9 by A1, A3, A4, A5, A7, Th13; :: thesis: verum

end;

end;