theorem Th55: :: BORSUK_4:58

for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex p1, p2 being Point of I[01] st
( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )