let s be rectangular FinSequence of (TOP-REAL 2); :: thesis: len s = 5
ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st s = SpStSeq D by Def2;
hence len s = 5 by Th40; :: thesis: verum