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