begin
:: deftheorem defines ^d FINTOPO3:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :
:: deftheorem defines Fcl FINTOPO3:def 3 :
:: deftheorem Def4 defines Fint FINTOPO3:def 4 :
:: deftheorem defines Fint FINTOPO3:def 5 :
theorem
theorem
theorem Th15:
theorem
theorem Th17:
theorem
theorem
theorem Th20:
theorem
theorem Th22:
theorem
theorem
theorem
theorem
theorem Th27:
theorem Th28:
theorem
theorem
:: deftheorem Def6 defines Finf FINTOPO3:def 6 :
:: deftheorem defines Finf FINTOPO3:def 7 :
:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :
:: deftheorem defines Fdfl FINTOPO3:def 9 :
theorem
theorem
theorem Th33:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th40:
theorem
theorem Th42:
theorem
theorem
theorem Th45:
theorem
:: deftheorem defines U_FT FINTOPO3:def 10 :
theorem
theorem
:: deftheorem defines are_mutually_symmetric FINTOPO3:def 11 :