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;

( 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;then ( li < li9 or li9 < li ) by XXREAL_0:1;

hence contradiction by A1, A2, A3, A4, A5, A7, Th13; :: thesis: verum

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;then ( ri < ri9 or ri9 < ri ) by XXREAL_0:1;

hence contradiction by A1, A2, A3, A4, A6, A8, Th13; :: thesis: verum