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 closed-interval Subset of REAL such that
A1: C c= D and
A2: D c= ].0 ,1.[ and
inf C = inf D and
sup C = sup D by Th82;
consider p1, p2 being Real such that
A3: p1 <= p2 and
A4: D = [.p1,p2.] by INTEGRA1:def 1;
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:83;
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