let C be non empty compact Subset of (TOP-REAL 2); W-bound (L~ (SpStSeq C)) = W-bound C
set S1 = LSeg ((NW-corner C),(NE-corner C));
set S2 = LSeg ((NE-corner C),(SE-corner C));
set S3 = LSeg ((SE-corner C),(SW-corner C));
set S4 = LSeg ((SW-corner C),(NW-corner C));
A1:
(SE-corner C) `1 = E-bound C
by EUCLID:52;
A2:
W-bound C <= E-bound C
by Th21;
A3:
(LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) is compact
by COMPTS_1:10;
A4:
(NE-corner C) `1 = E-bound C
by EUCLID:52;
then A5:
W-bound (LSeg ((NE-corner C),(SE-corner C))) = E-bound C
by A1, Th54;
A6:
(SW-corner C) `1 = W-bound C
by EUCLID:52;
A7:
(NW-corner C) `1 = W-bound C
by EUCLID:52;
then A8:
W-bound (LSeg ((SW-corner C),(NW-corner C))) = W-bound C
by A6, Th54;
A9: W-bound ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C)))) =
min ((W-bound (LSeg ((SE-corner C),(SW-corner C)))),(W-bound (LSeg ((SW-corner C),(NW-corner C)))))
by Th47
.=
min ((W-bound C),(W-bound C))
by A1, A6, A8, Th21, Th54
.=
W-bound C
;
A10:
L~ (SpStSeq C) = ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) \/ ((LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))))
by Th41;
A11:
(LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) is compact
by COMPTS_1:10;
W-bound ((LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C)))) =
min ((W-bound (LSeg ((NW-corner C),(NE-corner C)))),(W-bound (LSeg ((NE-corner C),(SE-corner C)))))
by Th47
.=
min ((E-bound C),(W-bound C))
by A7, A4, A5, Th21, Th54
.=
W-bound C
by A2, XXREAL_0:def 9
;
hence W-bound (L~ (SpStSeq C)) =
min ((W-bound C),(W-bound C))
by A10, A11, A3, A9, Th47
.=
W-bound C
;
verum