theorem Th56: :: PSCOMP_1:56
for X being non empty compact Subset of (TOP-REAL 2) holds S-most X c= LSeg ((S-min X),(S-max X))