theorem Th15: :: JORDAN1E:15
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )