let S be Subset of (TOP-REAL 2); :: thesis: len (SpStSeq S) = 5
thus len (SpStSeq S) = (len <*(NW-corner S),(NE-corner S),(SE-corner S)*>) + (len <*(SW-corner S),(NW-corner S)*>) by FINSEQ_1:22
.= (len <*(SW-corner S),(NW-corner S)*>) + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= 5 ; :: thesis: verum