begin
Lm1:
for T being empty TopSpace
for A being Subset of holds A = {}
;
theorem Th1:
theorem
canceled;
theorem
begin
theorem
canceled;
theorem Th5:
:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :
theorem
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem Th16:
begin
:: deftheorem Def2 defines is_an_accumulation_point_of TOPGEN_1:def 2 :
theorem Th17:
:: deftheorem Def3 defines Der TOPGEN_1:def 3 :
theorem Th18:
theorem Th19:
theorem
theorem
begin
:: deftheorem Def4 defines is_isolated_in TOPGEN_1:def 4 :
theorem
theorem Th23:
theorem Th24:
:: deftheorem Def5 defines isolated TOPGEN_1:def 5 :
theorem
begin
:: deftheorem Def6 defines Der TOPGEN_1:def 6 :
theorem
theorem
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
begin
:: deftheorem Def7 defines dense-in-itself TOPGEN_1:def 7 :
:: deftheorem defines dense-in-itself TOPGEN_1:def 8 :
theorem Th38:
:: deftheorem Def9 defines dense-in-itself TOPGEN_1:def 9 :
theorem Th39:
theorem Th40:
theorem
begin
:: deftheorem Def10 defines perfect TOPGEN_1:def 10 :
theorem Th42:
Lm2:
for T being TopSpace
for A being Subset of st A is closed & A is dense-in-itself holds
Der A = A
theorem Th43:
theorem Th44:
begin
:: deftheorem Def11 defines scattered TOPGEN_1:def 11 :
theorem Th45:
theorem
theorem Th47:
begin
:: deftheorem Def12 defines density TOPGEN_1:def 12 :
:: deftheorem Def13 defines separable TOPGEN_1:def 13 :
theorem
canceled;
theorem Th49:
begin
theorem
Lm3:
RAT = REAL \ IRRAT
theorem
theorem
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem