let C be non empty connected compact Subset of I[01]; 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; ( 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
; [.(lower_bound C9),(upper_bound C9).] = C9
assume
[.(lower_bound C9),(upper_bound C9).] <> C9
; 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; verum