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