begin
theorem Th1:
theorem Th2:
:: deftheorem defines U_FT FIN_TOPO:def 1 :
:: deftheorem defines SinglRel FIN_TOPO:def 2 :
:: deftheorem defines FT{0} FIN_TOPO:def 3 :
:: deftheorem Def4 defines filled FIN_TOPO:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem
canceled;
theorem
:: deftheorem FIN_TOPO:def 5 :
canceled;
:: deftheorem FIN_TOPO:def 6 :
canceled;
:: deftheorem defines ^delta FIN_TOPO:def 7 :
theorem Th10:
:: deftheorem defines ^deltai FIN_TOPO:def 8 :
:: deftheorem defines ^deltao FIN_TOPO:def 9 :
theorem
:: deftheorem defines ^i FIN_TOPO:def 10 :
:: deftheorem defines ^b FIN_TOPO:def 11 :
:: deftheorem defines ^s FIN_TOPO:def 12 :
:: deftheorem defines ^n FIN_TOPO:def 13 :
:: deftheorem defines ^f FIN_TOPO:def 14 :
:: deftheorem Def15 defines symmetric FIN_TOPO:def 15 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem
:: deftheorem Def16 defines open FIN_TOPO:def 16 :
:: deftheorem Def17 defines closed FIN_TOPO:def 17 :
:: deftheorem Def18 defines connected FIN_TOPO:def 18 :
:: deftheorem defines ^fb FIN_TOPO:def 19 :
:: deftheorem defines ^fi FIN_TOPO:def 20 :
theorem Th18:
theorem Th19:
theorem
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem