let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( (SW-corner X) `2 <= (W-min X) `2 & (SW-corner X) `2 <= (W-max X) `2 & (SW-corner X) `2 <= (NW-corner X) `2 & (W-min X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
set LX = W-most X;
A1: (W-min X) `2 = lower_bound (proj2 | (W-most X)) by EUCLID:52;
A2: (SW-corner X) `2 = lower_bound (proj2 | X) by EUCLID:52;
hence (SW-corner X) `2 <= (W-min X) `2 by A1, Th16, XBOOLE_1:17; :: thesis: ( (SW-corner X) `2 <= (W-max X) `2 & (SW-corner X) `2 <= (NW-corner X) `2 & (W-min X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
A3: (W-max X) `2 = upper_bound (proj2 | (W-most X)) by EUCLID:52;
then A4: (W-min X) `2 <= (W-max X) `2 by A1, Th7;
(SW-corner X) `2 <= (W-min X) `2 by A2, A1, Th16, XBOOLE_1:17;
hence A5: (SW-corner X) `2 <= (W-max X) `2 by A4, XXREAL_0:2; :: thesis: ( (SW-corner X) `2 <= (NW-corner X) `2 & (W-min X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
A6: (NW-corner X) `2 = upper_bound (proj2 | X) by EUCLID:52;
then A7: (W-max X) `2 <= (NW-corner X) `2 by A3, Th17, XBOOLE_1:17;
hence (SW-corner X) `2 <= (NW-corner X) `2 by A5, XXREAL_0:2; :: thesis: ( (W-min X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
thus (W-min X) `2 <= (W-max X) `2 by A1, A3, Th7; :: thesis: ( (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
thus (W-min X) `2 <= (NW-corner X) `2 by A4, A7, XXREAL_0:2; :: thesis: (W-max X) `2 <= (NW-corner X) `2
thus (W-max X) `2 <= (NW-corner X) `2 by A3, A6, Th17, XBOOLE_1:17; :: thesis: verum