let S be Subset of (TOP-REAL 2); :: thesis: 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:62;
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:27;
<*(SW-corner S),(NW-corner S)*> /. 1 = SW-corner S by FINSEQ_4:26;
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 Th10
.= ((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 ;
:: thesis: verum