begin
theorem Th1:
theorem Th2:
theorem
canceled;
theorem
begin
:: deftheorem Def1 defines anti-discrete TEX_4:def 1 :
:: deftheorem Def2 defines anti-discrete TEX_4:def 2 :
:: deftheorem Def3 defines anti-discrete TEX_4:def 3 :
:: deftheorem Def4 defines anti-discrete TEX_4:def 4 :
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def5 defines anti-discrete-set-family TEX_4:def 5 :
theorem Th10:
theorem
:: deftheorem defines MaxADSF TEX_4:def 6 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem Def7 defines maximal_anti-discrete TEX_4:def 7 :
theorem
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem defines MaxADSet TEX_4:def 8 :
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
:: deftheorem Def9 defines maximal_anti-discrete TEX_4:def 9 :
theorem Th29:
:: deftheorem defines maximal_anti-discrete TEX_4:def 10 :
:: deftheorem defines MaxADSet TEX_4:def 11 :
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
begin
:: deftheorem Def12 defines anti-discrete TEX_4:def 12 :
:: deftheorem defines anti-discrete TEX_4:def 13 :
:: deftheorem Def14 defines anti-discrete TEX_4:def 14 :
theorem
theorem
theorem
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
Lm1:
for X being non empty TopSpace
for x, y being Point of st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
theorem Th51:
theorem
:: deftheorem defines MaxADSet TEX_4:def 15 :
theorem Th53:
theorem
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem
theorem
theorem
theorem
theorem
begin
theorem Th68:
theorem Th69:
theorem
theorem
theorem
theorem
:: deftheorem Def16 defines maximal_anti-discrete TEX_4:def 16 :
theorem Th74:
:: deftheorem Def17 defines MaxADSspace TEX_4:def 17 :
Lm2:
for Y being non empty TopStruct
for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2
theorem
theorem
theorem
theorem
theorem
theorem
Lm3:
for Y being TopStruct
for A being Subset of holds the carrier of (Y | A) = A
theorem
theorem
:: deftheorem Def18 defines MaxADSspace TEX_4:def 18 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem