let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); 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; verum