let C be non empty compact Subset of I[01]; :: thesis: ( C c= ].0,1.[ implies ex p1, p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ ) )
assume C c= ].0,1.[ ; :: thesis: ex p1, p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
then consider D being non empty closed_interval Subset of REAL such that
A1: C c= D and
A2: D c= ].0,1.[ and
lower_bound C = lower_bound D and
upper_bound C = upper_bound D by Th54;
consider p1, p2 being Real such that
A3: p1 <= p2 and
A4: D = [.p1,p2.] by MEASURE5:14;
p1 in D by A3, A4, XXREAL_1:1;
then A5: p1 in ].0,1.[ by A2;
p2 in D by A3, A4, XXREAL_1:1;
then A6: p2 in ].0,1.[ by A2;
].0,1.[ c= [.0,1.] by XXREAL_1:25;
then reconsider p1 = p1, p2 = p2 as Point of I[01] by A5, A6, BORSUK_1:40;
take p1 ; :: thesis: ex p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
take p2 ; :: thesis: ( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
thus p1 <= p2 by A3; :: thesis: ( C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )
thus ( C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ ) by A1, A2, A4; :: thesis: verum