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