begin
theorem
theorem
canceled;
theorem Th3:
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th11:
theorem Th12:
Lm1:
for T being 1-sorted
for F being Subset-Family of T st COMPLEMENT F is finite holds
F is finite
theorem Th13:
:: deftheorem Def1 defines open TOPS_2:def 1 :
:: deftheorem Def2 defines closed TOPS_2:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th26:
theorem Th27:
theorem
theorem
theorem
canceled;
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem
theorem
canceled;
theorem Th38:
:: deftheorem Def3 defines | TOPS_2:def 3 :
theorem
canceled;
theorem
theorem Th41:
theorem
theorem
theorem Th44:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem Th52:
theorem
canceled;
theorem
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem
:: deftheorem Def4 defines /" TOPS_2:def 4 :
theorem
canceled;
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem Th66:
theorem Th67:
theorem Th68:
:: deftheorem Def5 defines being_homeomorphism TOPS_2:def 5 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem Th75:
theorem
begin
theorem
theorem Th1:
theorem