begin
:: deftheorem Def1 defines is_parallel_to RUSUB_5:def 1 :
theorem
theorem Th2:
theorem Th3:
:: deftheorem defines - RUSUB_5:def 2 :
theorem Th4:
theorem
theorem
theorem
theorem Th8:
theorem Th9:
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
begin
:: deftheorem Def3 defines Ort_Comp RUSUB_5:def 3 :
:: deftheorem Def4 defines Ort_Comp RUSUB_5:def 4 :
theorem
theorem
theorem
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem
theorem
theorem
begin
:: deftheorem Def5 defines Family_open_set RUSUB_5:def 5 :
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
:: deftheorem defines TopUnitSpace RUSUB_5:def 6 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th50:
theorem
theorem
theorem Th53:
theorem