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 )
A1: (NW-corner X) `1 = inf (proj1 | X) by EUCLID:56;
set LX = N-most X;
A2: (N-min X) `1 = inf (proj1 | (N-most X)) by EUCLID:56;
A3: (N-max X) `1 = sup (proj1 | (N-most X)) by EUCLID:56;
A4: (NE-corner X) `1 = sup (proj1 | X) by EUCLID:56;
A5: (NW-corner X) `1 <= (N-min X) `1 by A1, A2, Th62, XBOOLE_1:17;
A6: (N-min X) `1 <= (N-max X) `1 by A2, A3, Th53;
A7: (N-max X) `1 <= (NE-corner X) `1 by A3, A4, Th63, XBOOLE_1:17;
thus (NW-corner X) `1 <= (N-min X) `1 by A1, A2, Th62, 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 )
thus (NW-corner X) `1 <= (N-max X) `1 by A5, A6, 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 )
hence (NW-corner X) `1 <= (NE-corner X) `1 by A7, 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 A2, A3, Th53; :: 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 A6, A7, XXREAL_0:2; :: thesis: (N-max X) `1 <= (NE-corner X) `1
thus (N-max X) `1 <= (NE-corner X) `1 by A3, A4, Th63, XBOOLE_1:17; :: thesis: verum