let S be Subset of (TOP-REAL 2); L~ (SpStSeq S) = ((LSeg ((NW-corner S),(NE-corner S))) \/ (LSeg ((NE-corner S),(SE-corner S)))) \/ ((LSeg ((SE-corner S),(SW-corner S))) \/ (LSeg ((SW-corner S),(NW-corner S))))
len <*(NW-corner S),(NE-corner S),(SE-corner S)*> = 3
by FINSEQ_1:45;
then A1:
<*(NW-corner S),(NE-corner S),(SE-corner S)*> /. (len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) = SE-corner S
by FINSEQ_4:18;
<*(SW-corner S),(NW-corner S)*> /. 1 = SW-corner S
by FINSEQ_4:17;
hence L~ (SpStSeq S) =
((L~ <*(NW-corner S),(NE-corner S),(SE-corner S)*>) \/ (LSeg ((SE-corner S),(SW-corner S)))) \/ (L~ <*(SW-corner S),(NW-corner S)*>)
by A1, SPPOL_2:23
.=
((L~ <*(NW-corner S),(NE-corner S),(SE-corner S)*>) \/ (LSeg ((SE-corner S),(SW-corner S)))) \/ (LSeg ((SW-corner S),(NW-corner S)))
by SPPOL_2:21
.=
(((LSeg ((NW-corner S),(NE-corner S))) \/ (LSeg ((NE-corner S),(SE-corner S)))) \/ (LSeg ((SE-corner S),(SW-corner S)))) \/ (LSeg ((SW-corner S),(NW-corner S)))
by Th8
.=
((LSeg ((NW-corner S),(NE-corner S))) \/ (LSeg ((NE-corner S),(SE-corner S)))) \/ ((LSeg ((SE-corner S),(SW-corner S))) \/ (LSeg ((SW-corner S),(NW-corner S))))
by XBOOLE_1:4
;
verum