consider C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
SpStSeq C is special_circular_sequence ;
hence ex b₁ being special_circular_sequence st b₁ is rectangular ; :: thesis: verum