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: 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;
A2: W-bound C <= E-bound C by Th23;
A3: (NW-corner C) `1 = W-bound C by EUCLID:56;
A4: (NE-corner C) `1 = E-bound C by EUCLID:56;
A5: (SE-corner C) `1 = E-bound C by EUCLID:56;
A6: (SW-corner C) `1 = W-bound C by EUCLID:56;
A7: W-bound (LSeg (NE-corner C),(SE-corner C)) = E-bound C by A4, A5, Th62;
A8: W-bound (LSeg (SW-corner C),(NW-corner C)) = W-bound C by A3, A6, Th62;
A9: (LSeg (NW-corner C),(NE-corner C)) \/ (LSeg (NE-corner C),(SE-corner C)) is compact by COMPTS_1:19;
A10: 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 A3, A4, A7, Th23, Th62
.= W-bound C by A2, XXREAL_0:def 9 ;
A11: (LSeg (SE-corner C),(SW-corner C)) \/ (LSeg (SW-corner C),(NW-corner C)) is compact by COMPTS_1:19;
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 A5, A6, A8, Th23, Th62
.= W-bound C ;
hence W-bound (L~ (SpStSeq C)) = min (W-bound C),(W-bound C) by A1, A9, A10, A11, Th54
.= W-bound C ;
:: thesis: verum