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