begin
Lm1:
for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 )
theorem
theorem Th2:
theorem Th3:
Lm2:
for T being TopStruct
for A being Subset of holds
( A is open iff ([#] T) \ A is closed )
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
:: deftheorem Def10 defines Balls FRECHET:def 1 :
theorem Th11:
theorem Th12:
theorem Th13:
for
A,
B being
set st
B c= A holds
(id A) .: B = B
theorem
canceled;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
begin
:: deftheorem Def1 defines first-countable FRECHET:def 2 :
theorem Th21:
theorem
:: deftheorem Def2 defines is_convergent_to FRECHET:def 3 :
theorem Th23:
:: deftheorem Def3 defines convergent FRECHET:def 4 :
:: deftheorem Def4 defines Lim FRECHET:def 5 :
:: deftheorem Def5 defines Frechet FRECHET:def 6 :
:: deftheorem defines sequential FRECHET:def 7 :
theorem Th24:
theorem
canceled;
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def7 defines REAL? FRECHET:def 8 :
Lm3:
{REAL } c= the carrier of REAL?
theorem
canceled;
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
begin
theorem
canceled;
theorem
theorem