let Gi be non trivial finite Subset of REAL; 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; ( 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
; ( 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;