let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).]
L~ (SpStSeq D) = ((LSeg (NW-corner D),(NE-corner D)) \/ (LSeg (NE-corner D),(SE-corner D))) \/ ((LSeg (SE-corner D),(SW-corner D)) \/ (LSeg (SW-corner D),(NW-corner D))) by Th43
.= ((LSeg (SW-corner D),(NW-corner D)) \/ ((LSeg (NW-corner D),(NE-corner D)) \/ (LSeg (NE-corner D),(SE-corner D)))) \/ (LSeg (SE-corner D),(SW-corner D)) by XBOOLE_1:4
.= (((LSeg (SW-corner D),(NW-corner D)) \/ (LSeg (NW-corner D),(NE-corner D))) \/ (LSeg (NE-corner D),(SE-corner D))) \/ (LSeg (SE-corner D),(SW-corner D)) by XBOOLE_1:4
.= ((LSeg (SW-corner D),(NW-corner D)) \/ (LSeg (NW-corner D),(NE-corner D))) \/ ((LSeg (NE-corner D),(SE-corner D)) \/ (LSeg (SE-corner D),(SW-corner D))) by XBOOLE_1:4 ;
hence L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).] by SPPOL_2:def 3; :: thesis: verum