let Gi be non trivial finite Subset of REAL ; :: thesis: for li, ri, li' being Real st [li,ri] is Gap of Gi & [li',ri] is Gap of Gi holds
li = li'
let li, ri, li' be Real; :: thesis: ( [li,ri] is Gap of Gi & [li',ri] is Gap of Gi implies li = li' )
A1: ( li <= li' & li' <= li implies li = li' ) by XXREAL_0:1;
assume A2: ( [li,ri] is Gap of Gi & [li',ri] is Gap of Gi ) ; :: thesis: li = li'
then A3: ( li in Gi & li' in Gi ) by Th17;

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, Th17;

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

( li' <= li or ( li < li' & li' < ri ) or ri <= li' ) ;
hence li = li' by A1, A2, A3, A4, Th17; :: thesis: verum

end;

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

( li' < ri or ( ri <= li' & li' <= li ) or li < li' ) ;
hence li = li' by A1, A2, A3, A5, Th17; :: thesis: verum

end;

end;