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 Th41
.= ((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