let C be non empty connected compact Subset of I[01]; :: thesis: for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9
let C9 be Subset of REAL; :: thesis: ( C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 implies [.(lower_bound C9),(upper_bound C9).] = C9 )
assume that
A1: C = C9 and
A2: [.(lower_bound C9),(upper_bound C9).] c= C9 ; :: thesis: [.(lower_bound C9),(upper_bound C9).] = C9
assume [.(lower_bound C9),(upper_bound C9).] <> C9 ; :: thesis: contradiction
then not C9 c= [.(lower_bound C9),(upper_bound C9).] by A2, XBOOLE_0:def 10;
then consider c being object such that
A3: c in C9 and
A4: not c in [.(lower_bound C9),(upper_bound C9).] ;
reconsider c = c as Real by A3;
A5: c <= upper_bound C9 by A1, A3, Th23;
lower_bound C9 <= c by A1, A3, Th23;
hence contradiction by A4, A5, XXREAL_1:1; :: thesis: verum