theorem Th46: :: PSCOMP_1:46

for X being non empty compact Subset of (TOP-REAL 2) holds
( (SE-corner X) `2 <= (E-min X) `2 & (SE-corner X) `2 <= (E-max X) `2 & (SE-corner X) `2 <= (NE-corner X) `2 & (E-min X) `2 <= (E-max X) `2 & (E-min X) `2 <= (NE-corner X) `2 & (E-max X) `2 <= (NE-corner X) `2 )