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