let s be rectangular FinSequence of ; :: thesis: len s = 5
ex D being non empty compact non horizontal non vertical Subset of st s = SpStSeq D by Def2;
hence len s = 5 by Th42; :: thesis: verum