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