begin
theorem
canceled;
theorem
theorem
canceled;
theorem Th4:
begin
:: deftheorem KURATO_2:def 1 :
canceled;
:: deftheorem KURATO_2:def 2 :
canceled;
:: deftheorem Def3 defines lim_inf KURATO_2:def 3 :
:: deftheorem Def4 defines lim_sup KURATO_2:def 4 :
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem Th17:
theorem Th18:
theorem
theorem
begin
theorem Th21:
:: deftheorem Def5 defines non-ascending KURATO_2:def 5 :
:: deftheorem Def6 defines non-descending KURATO_2:def 6 :
theorem
canceled;
theorem
canceled;
theorem Th24:
theorem
theorem
begin
:: deftheorem Def7 defines convergent KURATO_2:def 7 :
theorem
:: deftheorem KURATO_2:def 8 :
canceled;
:: deftheorem Def9 defines Lim_K KURATO_2:def 9 :
theorem
begin
theorem
canceled;
theorem Th30:
theorem
canceled;
theorem Th32:
theorem Th33:
theorem
Lm1:
for T being non empty TopSpace
for x being Point of T
for y being Point of TopStruct(# the carrier of T,the topology of T #)
for A being set st x = y holds
( A is Basis of x iff A is Basis of y )
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th45:
theorem
canceled;
theorem
begin
:: deftheorem KURATO_2:def 10 :
canceled;
:: deftheorem Def11 defines Lim_inf KURATO_2:def 11 :
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem Th52:
theorem
theorem
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem
theorem Th62:
theorem
theorem
begin
:: deftheorem Def12 defines Lim_sup KURATO_2:def 12 :
theorem
theorem Th66:
theorem Th67:
theorem
theorem Th69:
theorem
theorem
theorem Th72:
theorem
theorem Th74:
theorem
theorem