let C be non empty compact Subset of (TOP-REAL 2); :: thesis: N-bound (L~ (SpStSeq C)) = N-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: (NW-corner C) `2 = N-bound C by EUCLID:56;
A2: S-bound C <= N-bound C by Th24;
A3: (LSeg (SE-corner C),(SW-corner C)) \/ (LSeg (SW-corner C),(NW-corner C)) is compact by COMPTS_1:19;
A4: (SW-corner C) `2 = S-bound C by EUCLID:56;
then A5: N-bound (LSeg (SW-corner C),(NW-corner C)) = N-bound C by A1, Th24, Th64;
A6: (SE-corner C) `2 = S-bound C by EUCLID:56;
A7: (NE-corner C) `2 = N-bound C by EUCLID:56;
then A8: N-bound (LSeg (NE-corner C),(SE-corner C)) = N-bound C by A6, Th24, Th64;
A9: N-bound ((LSeg (NW-corner C),(NE-corner C)) \/ (LSeg (NE-corner C),(SE-corner C))) = max (N-bound (LSeg (NW-corner C),(NE-corner C))),(N-bound (LSeg (NE-corner C),(SE-corner C))) by Th56
.= max (N-bound C),(N-bound C) by A1, A7, A8, Th64
.= N-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;
N-bound ((LSeg (SE-corner C),(SW-corner C)) \/ (LSeg (SW-corner C),(NW-corner C))) = max (N-bound (LSeg (SE-corner C),(SW-corner C))),(N-bound (LSeg (SW-corner C),(NW-corner C))) by Th56
.= max (S-bound C),(N-bound C) by A6, A4, A5, Th64
.= N-bound C by A2, XXREAL_0:def 10 ;
hence N-bound (L~ (SpStSeq C)) = max (N-bound C),(N-bound C) by A10, A11, A9, A3, Th56
.= N-bound C ;
:: thesis: verum