begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines trivial YELLOW_8:def 1 :
begin
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th15:
theorem Th16:
begin
theorem
theorem Th18:
theorem Th19:
theorem
begin
:: deftheorem Def2 defines -quasi_basis YELLOW_8:def 2 :
theorem Th21:
theorem
theorem
:: deftheorem Def3 defines Baire YELLOW_8:def 3 :
theorem
begin
:: deftheorem Def4 defines irreducible YELLOW_8:def 4 :
:: deftheorem Def5 defines is_dense_point_of YELLOW_8:def 5 :
theorem
theorem Th26:
:: deftheorem Def6 defines sober YELLOW_8:def 6 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem Def7 defines CofinTop YELLOW_8:def 7 :
theorem Th34:
theorem Th35:
begin
theorem Th36:
theorem