for C being non empty connected compact Subset of I[01] holds C is non empty closed_interval Subset of REAL