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 C' = C as Subset of REAL by BORSUK_1:83, XBOOLE_1:1;
A2: C' is closed by Th52;
A3: ( C' is bounded_below & C' is bounded_above ) by Th50;
then A4: inf C' in C' by A2, RCOMP_1:31;
A5: sup C' in C' by A2, A3, RCOMP_1:30;
reconsider D = [.(inf C'),(sup C').] as Subset of REAL ;
A6: C c= D

proof

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

end;

consider x being Element of C';
A8: C' is bounded by A3;
then A9: lower_bound C' <= upper_bound C' by SEQ_4:24;
A10: D is non empty connected compact Subset of I[01] by A4, A5, 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: ( inf C' = inf D & sup C' = sup D ) by A9, XXREAL_1:66;
A14: not 0 in D

proof

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

end;

A15: not 1 in D

proof

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

end;

A16: 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 A17: x in D ; :: thesis: x in ].0 ,1.[
thus x in ].0 ,1.[ by A10, A14, A15, A17, BORSUK_1:83, XXREAL_1:5; :: thesis: verum

end;

reconsider D = D as closed-interval Subset of REAL by A9, 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 A6, A9, A12, A16, XXREAL_1:66; :: thesis: verum