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 :
theorem Th12:
:: deftheorem defines Lower_Seq JORDAN1E:def 2 :
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