let C be non empty compact Subset of I[01]; :: thesis: ( C c= ].0,1.[ implies ex D being non empty closed_interval Subset of REAL st
( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D ) )
assume A1: C c= ].0,1.[ ; :: thesis: ex D being non empty closed_interval Subset of REAL st
( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D )
reconsider C9 = C as Subset of REAL by BORSUK_1:40, XBOOLE_1:1;
reconsider D = [.(lower_bound C9),(upper_bound C9).] as Subset of REAL ;
A2: ( C9 is bounded_below & C9 is bounded_above ) by Th22;
then A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
A4: C c= D
proof
let x be object ; :: 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 ;
A6: x9 <= upper_bound C9 by A5, Th23;
lower_bound C9 <= x9 by A5, Th23;
hence x in D by A6, XXREAL_1:1; :: thesis: verum
end;
A7: C9 is closed by Th24;
then A8: lower_bound C9 in C9 by Th22, RCOMP_1:13;
A9: upper_bound C9 in C9 by A7, Th22, RCOMP_1:12;
then A10: D is non empty connected compact Subset of I[01] by A2, A8, Th21, SEQ_4:11;
then A11: D is non empty closed_interval Subset of REAL by Th27;
then A12: D = [.(lower_bound D),(upper_bound D).] by INTEGRA1:4;
then A13: upper_bound C9 = upper_bound D by A3, XXREAL_1:66;
A14: not 1 in D
proof
assume 1 in D ; :: thesis: contradiction
then upper_bound D >= 1 by A11, INTEGRA2:1;
hence contradiction by A1, A9, A13, XXREAL_1:4; :: thesis: verum
end;
A15: lower_bound C9 = lower_bound D by A3, A12, XXREAL_1:66;
A16: not 0 in D
proof
assume 0 in D ; :: thesis: contradiction
then lower_bound D <= 0 by A11, INTEGRA2:1;
hence contradiction by A1, A8, A15, XXREAL_1:4; :: thesis: verum
end;
A17: D c= ].0,1.[ by A10, A16, A14, BORSUK_1:40, XXREAL_1:5;
reconsider D = D as non empty closed_interval Subset of REAL by A3, MEASURE5:14;
take D ; :: thesis: ( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D )
thus ( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D ) by A4, A3, A12, A17, XXREAL_1:66; :: thesis: verum