let X be non empty compact Subset of (TOP-REAL 2); ( (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; ( (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; ( (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; ( (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; ( (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; (N-max X) `1 <= (NE-corner X) `1
thus
(N-max X) `1 <= (NE-corner X) `1
by A3, A6, Th17, XBOOLE_1:17; verum