begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem
theorem
theorem Th9:
theorem Th10:
theorem
begin
:: deftheorem defines Upper_Seq JORDAN1E:def 1 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)));
theorem Th12:
:: deftheorem defines Lower_Seq JORDAN1E:def 2 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n)));
theorem Th13:
registration
let C be
compact non
horizontal non
vertical Subset of
(TOP-REAL 2);
let n be
Element of
NAT ;
cluster Upper_Seq C,
n -> one-to-one special unfolded s.n.c. ;
coherence
( Upper_Seq C,n is one-to-one & Upper_Seq C,n is special & Upper_Seq C,n is unfolded & Upper_Seq C,n is s.n.c. )
cluster Lower_Seq C,
n -> one-to-one special unfolded s.n.c. ;
coherence
( Lower_Seq C,n is one-to-one & Lower_Seq C,n is special & Lower_Seq C,n is unfolded & Lower_Seq C,n is s.n.c. )
end;
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
theorem Th19:
theorem
theorem
theorem
theorem
theorem
theorem
theorem