let Gi be non trivial finite Subset of ; :: thesis: for ri, li, ri', li' being Real st ri < li & [li,ri] is Gap of Gi & ri' < li' & [li',ri'] is Gap of Gi holds
( li = li' & ri = ri' )
let ri, li, ri', li' be Real; :: thesis: ( ri < li & [li,ri] is Gap of Gi & ri' < li' & [li',ri'] is Gap of Gi implies ( li = li' & ri = ri' ) )
assume that
A1: ri < li and
A2: [li,ri] is Gap of Gi and
A3: ri' < li' and
A4: [li',ri'] is Gap of Gi ; :: thesis: ( li = li' & ri = ri' )
A5: li in Gi by A2, Th17;
A6: ri in Gi by A2, Th17;
A7: li' in Gi by A4, Th17;
A8: ri' in Gi by A4, Th17;

hereby :: thesis: ri = ri'

assume li <> li' ; :: thesis: contradiction
then ( li < li' or li' < li ) by XXREAL_0:1;
hence contradiction by A1, A2, A3, A4, A5, A7, Th17; :: thesis: verum

end;

hereby :: thesis: verum

assume ri <> ri' ; :: thesis: contradiction
then ( ri < ri' or ri' < ri ) by XXREAL_0:1;
hence contradiction by A1, A2, A3, A4, A6, A8, Th17; :: thesis: verum

end;