let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( S-min C in C & S-max C in C )
A1: S-most C c= C by XBOOLE_1:17;
( S-min C in S-most C & S-max C in S-most C ) by PSCOMP_1:121;
hence ( S-min C in C & S-max C in C ) by A1; :: thesis: verum