consider C being non empty compact non horizontal non vertical Subset of ;
SpStSeq C is special_circular_sequence ;
hence ex b₁ being special_circular_sequence st b₁ is rectangular ; :: thesis: verum