begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem
:: deftheorem Def1 defines incl YELLOW_9:def 1 :
:: deftheorem defines +id YELLOW_9:def 2 :
:: deftheorem defines opp+id YELLOW_9:def 3 :
theorem
theorem
begin
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem Th37:
theorem Th38:
theorem
begin
theorem Th40:
theorem Th41:
theorem
theorem
begin
:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :
theorem
theorem
theorem
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem
Lm2:
for S being TopStruct ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )
begin
:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :
theorem Th53:
:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :
theorem
theorem
theorem
theorem
theorem
theorem Th59:
theorem Th60:
theorem