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