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

hereby :: thesis: ri = ri9

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

end;

hereby :: thesis: verum

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

end;