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