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