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