begin
theorem
theorem Th2:
theorem
theorem
theorem
:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :
:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :
theorem
theorem
theorem Th8:
:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :
theorem
theorem
theorem
:: deftheorem Def4 defines P_A FINTOPO2:def 4 :
theorem
theorem
theorem
:: deftheorem Def5 defines P_e FINTOPO2:def 5 :
theorem
theorem
theorem
theorem
begin
:: deftheorem defines U_FMT FINTOPO2:def 6 :
:: deftheorem defines NeighSp FINTOPO2:def 7 :
:: deftheorem Def8 defines Fo_filled FINTOPO2:def 8 :
:: deftheorem defines ^Fodelta FINTOPO2:def 9 :
theorem
canceled;
theorem Th20:
:: deftheorem defines ^Fob FINTOPO2:def 10 :
theorem Th21:
:: deftheorem defines ^Foi FINTOPO2:def 11 :
theorem Th22:
:: deftheorem defines ^Fos FINTOPO2:def 12 :
theorem Th23:
:: deftheorem defines ^Fon FINTOPO2:def 13 :
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
theorem
:: deftheorem defines ^Fodel_i FINTOPO2:def 14 :
:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :
theorem
:: deftheorem Def16 defines Fo_open FINTOPO2:def 16 :
:: deftheorem Def17 defines Fo_closed FINTOPO2:def 17 :
theorem
theorem
theorem
theorem