theorem :: PSCOMP_1:63

for P being Subset of (TOP-REAL 2) st E-min P = S-max P holds
E-min P = SE-corner P