theorem :: JORDAN1E:16

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}