for X being non empty connected compact Subset of R^1 holds X is non empty closed_interval Subset of REAL