let C be non empty compact Subset of (TOP-REAL 2); :: thesis: 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:56;
A2: W-bound C <= E-bound C by Th23;
A3: (LSeg ((SE-corner C),(SW-corner C))) \/ (LSeg ((SW-corner C),(NW-corner C))) is compact by COMPTS_1:19;
A4: (NE-corner C) `1 = E-bound C by EUCLID:56;
then A5: W-bound (LSeg ((NE-corner C),(SE-corner C))) = E-bound C by A1, Th62;
A6: (SW-corner C) `1 = W-bound C by EUCLID:56;
A7: (NW-corner C) `1 = W-bound C by EUCLID:56;
then A8: W-bound (LSeg ((SW-corner C),(NW-corner C))) = W-bound C by A6, Th62;
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 Th54
.= min ((W-bound C),(W-bound C)) by A1, A6, A8, Th23, Th62
.= 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 Th43;
A11: (LSeg ((NW-corner C),(NE-corner C))) \/ (LSeg ((NE-corner C),(SE-corner C))) is compact by COMPTS_1:19;
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 Th54
.= min ((E-bound C),(W-bound C)) by A7, A4, A5, Th23, Th62
.= 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, Th54
.= W-bound C ;
:: thesis: verum