let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( (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 )
set LX = E-most X;
A1: (E-min X) `2 = inf (proj2 | (E-most X)) by EUCLID:56;
A2: (SE-corner X) `2 = inf (proj2 | X) by EUCLID:56;
hence (SE-corner X) `2 <= (E-min X) `2 by A1, Th62, XBOOLE_1:17; :: thesis: ( (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 )
A3: (E-max X) `2 = sup (proj2 | (E-most X)) by EUCLID:56;
then A4: (E-min X) `2 <= (E-max X) `2 by A1, Th53;
(SE-corner X) `2 <= (E-min X) `2 by A2, A1, Th62, XBOOLE_1:17;
hence A5: (SE-corner X) `2 <= (E-max X) `2 by A4, XXREAL_0:2; :: thesis: ( (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 )
A6: (NE-corner X) `2 = sup (proj2 | X) by EUCLID:56;
then A7: (E-max X) `2 <= (NE-corner X) `2 by A3, Th63, XBOOLE_1:17;
hence (SE-corner X) `2 <= (NE-corner X) `2 by A5, XXREAL_0:2; :: thesis: ( (E-min X) `2 <= (E-max X) `2 & (E-min X) `2 <= (NE-corner X) `2 & (E-max X) `2 <= (NE-corner X) `2 )
thus (E-min X) `2 <= (E-max X) `2 by A1, A3, Th53; :: thesis: ( (E-min X) `2 <= (NE-corner X) `2 & (E-max X) `2 <= (NE-corner X) `2 )
thus (E-min X) `2 <= (NE-corner X) `2 by A4, A7, XXREAL_0:2; :: thesis: (E-max X) `2 <= (NE-corner X) `2
thus (E-max X) `2 <= (NE-corner X) `2 by A3, A6, Th63, XBOOLE_1:17; :: thesis: verum