let C be non empty compact Subset of I[01] ; :: thesis: ( C c= ].0 ,1.[ implies ex D being closed-interval Subset of REAL st
( C c= D & D c= ].0 ,1.[ & inf C = inf D & sup C = sup D ) )
assume A1: C c= ].0 ,1.[ ; :: thesis: ex D being closed-interval Subset of REAL st
( C c= D & D c= ].0 ,1.[ & inf C = inf D & sup C = sup D )
reconsider C9 = C as Subset of REAL by BORSUK_1:83, XBOOLE_1:1;
reconsider D = [.(inf C9),(sup C9).] as Subset of REAL ;
A2: ( C9 is bounded_below & C9 is bounded_above ) by Th50;
then A3: lower_bound C9 <= upper_bound C9 by SEQ_4:24;
A4: C c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in D )
assume A5: x in C ; :: thesis: x in D
then x in the carrier of I[01] ;
then reconsider x9 = x as Real by BORSUK_1:83;
A6: x9 <= sup C9 by A5, Th51;
inf C9 <= x9 by A5, Th51;
hence x in D by A6, XXREAL_1:1; :: thesis: verum

end;

A7: C9 is closed by Th52;
then A8: inf C9 in C9 by Th50, RCOMP_1:31;
A9: sup C9 in C9 by A7, Th50, RCOMP_1:30;
then A10: D is non empty connected compact Subset of I[01] by A2, A8, Th49, SEQ_4:24;
then A11: D is closed-interval Subset of REAL by Th55;
then A12: D = [.(inf D),(sup D).] by INTEGRA1:5;
then A13: sup C9 = sup D by A3, XXREAL_1:66;
A14: not 1 in D

proof

assume 1 in D ; :: thesis: contradiction
then sup D >= 1 by A11, INTEGRA2:1;
hence contradiction by A1, A9, A13, XXREAL_1:4; :: thesis: verum

end;

A15: inf C9 = inf D by A3, A12, XXREAL_1:66;
A16: not 0 in D

proof

assume 0 in D ; :: thesis: contradiction
then inf D <= 0 by A11, INTEGRA2:1;
hence contradiction by A1, A8, A15, XXREAL_1:4; :: thesis: verum

end;

A17: D c= ].0 ,1.[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in ].0 ,1.[ )
assume x in D ; :: thesis: x in ].0 ,1.[
hence x in ].0 ,1.[ by A10, A16, A14, BORSUK_1:83, XXREAL_1:5; :: thesis: verum

end;

reconsider D = D as closed-interval Subset of REAL by A3, INTEGRA1:def 1;
take D ; :: thesis: ( C c= D & D c= ].0 ,1.[ & inf C = inf D & sup C = sup D )
thus ( C c= D & D c= ].0 ,1.[ & inf C = inf D & sup C = sup D ) by A4, A3, A12, A17, XXREAL_1:66; :: thesis: verum
consider x being Element of C9;