let C be non empty connected compact Subset of I[01] ; :: thesis: for C' being Subset of REAL st C = C' & [.(inf C'),(sup C').] c= C' holds
[.(inf C'),(sup C').] = C'
let C' be Subset of REAL ; :: thesis: ( C = C' & [.(inf C'),(sup C').] c= C' implies [.(inf C'),(sup C').] = C' )
assume A1: ( C = C' & [.(inf C'),(sup C').] c= C' ) ; :: thesis: [.(inf C'),(sup C').] = C'
assume [.(inf C'),(sup C').] <> C' ; :: thesis: contradiction
then not C' c= [.(inf C'),(sup C').] by A1, XBOOLE_0:def 10;
then consider c being set such that
A2: ( c in C' & not c in [.(inf C'),(sup C').] ) by TARSKI:def 3;
reconsider c = c as real number by A2;
( inf C' <= c & c <= sup C' ) by A1, A2, Th51;
hence contradiction by A2, XXREAL_1:1; :: thesis: verum