:: Maximal Anti-Discrete Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

:: 1. Properties of the Closure and the Interior Operations.
registration
let X be non empty TopSpace;
let A be non empty Subset of X;
cluster Cl A ->  non empty ;
coherence
 not Cl A is empty by PCOMPS_1:2;
end;

registration
let X be TopSpace;
let A be empty Subset of X;
cluster Cl A ->  empty ;
coherence
 Cl A is empty by PRE_TOPC:22;
end;

registration
let X be non empty TopSpace;
let A be non proper Subset of X;
cluster Cl A ->  non proper ;
coherence
 not Cl A is proper
proofend;
end;

registration
let X be non trivial TopSpace;
let A be non trivial Subset of X;
cluster Cl A ->  non trivial ;
coherence
 not Cl A is trivial
proofend;
end;

theorem Th1: :: TEX_4:1
for X being non empty TopSpace
for A being Subset of X holds Cl A = meet  {  F where F is Subset of X : ( F is closed & A c= F )  }
proofend;

theorem Th2: :: TEX_4:2
for X being non empty TopSpace
for x being Point of X holds Cl {x} = meet  {  F where F is Subset of X : ( F is closed & x in F )  }
proofend;

registration
let X be non empty TopSpace;
let A be non proper Subset of X;
cluster Int A ->  non proper ;
coherence
 not Int A is proper
proofend;
end;

registration
let X be non empty TopSpace;
let A be proper Subset of X;
cluster Int A ->  proper ;
coherence
 Int A is proper
proofend;
end;

registration
let X be non empty TopSpace;
let A be empty Subset of X;
cluster Int A ->  empty ;
coherence
 Int A is empty ;
end;

theorem :: TEX_4:3
for X being non empty TopSpace
for A being Subset of X holds Int A = union  {  G where G is Subset of X : ( G is open & G c= A )  }
proofend;

begin

:: 2. Anti-discrete Subsets of Topological Structures.
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is anti-discrete  means :Def1: :: TEX_4:def 1
 for x being Point of Y
for G being Subset of Y st G is open & x in G & x in IT holds
IT c= G;
end;

:: deftheorem Def1 defines anti-discrete TEX_4:def_1_:_
 for Y being TopStruct
for IT being Subset of Y holds
( IT is anti-discrete iff for x being Point of Y
for G being Subset of Y st G is open & x in G & x in IT holds
IT c= G );

definition
let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete  means :Def2: :: TEX_4:def 2
 for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F;
compatibility
 ( A is anti-discrete iff for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F )
proofend;
end;

:: deftheorem Def2 defines anti-discrete TEX_4:def_2_:_
 for Y being non empty TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F );

definition
let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete  means :Def3: :: TEX_4:def 3
 for G being Subset of Y holds
( not G is open or A misses G or A c= G );
compatibility
 ( A is anti-discrete iff for G being Subset of Y holds
( not G is open or A misses G or A c= G ) )
proofend;
end;

:: deftheorem Def3 defines anti-discrete TEX_4:def_3_:_
 for Y being TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for G being Subset of Y holds
( not G is open or A misses G or A c= G ) );

definition
let Y be TopStruct ;
let A be Subset of Y;
redefine attr A is anti-discrete  means :Def4: :: TEX_4:def 4
 for F being Subset of Y holds
( not F is closed or A misses F or A c= F );
compatibility
 ( A is anti-discrete iff for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) )
proofend;
end;

:: deftheorem Def4 defines anti-discrete TEX_4:def_4_:_
 for Y being TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) );

theorem Th4: :: TEX_4:4
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds
D1 is anti-discrete
proofend;

theorem Th5: :: TEX_4:5
for Y being non empty TopStruct
for A, B being Subset of Y st B c= A & A is anti-discrete holds
B is anti-discrete
proofend;

theorem Th6: :: TEX_4:6
for Y being non empty TopStruct
for x being Point of Y holds {x} is anti-discrete
proofend;

theorem Th7: :: TEX_4:7
for Y being non empty TopStruct
for A being empty Subset of Y holds A is anti-discrete
proofend;

definition
let Y be TopStruct ;
let IT be Subset-Family of Y;
attrIT is anti-discrete-set-family  means :Def5: :: TEX_4:def 5
 for A being Subset of Y st A in IT holds
A is anti-discrete ;
end;

:: deftheorem Def5 defines anti-discrete-set-family TEX_4:def_5_:_
 for Y being TopStruct
for IT being Subset-Family of Y holds
( IT is anti-discrete-set-family iff for A being Subset of Y st A in IT holds
A is anti-discrete );

theorem Th8: :: TEX_4:8
for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family &amp; meet F <> {} holds
union F is anti-discrete
proofend;

theorem :: TEX_4:9
for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family holds
meet F is anti-discrete
proofend;

definition
let Y be TopStruct ;
let x be Point of Y;
func MaxADSF x ->  Subset-Family of Y equals :: TEX_4:def 6
 {  A where A is Subset of Y : ( A is anti-discrete &amp; x in A )  }  ;
coherence
  {  A where A is Subset of Y : ( A is anti-discrete &amp; x in A )  }  is Subset-Family of Y
proofend;
end;

:: deftheorem  defines MaxADSF TEX_4:def_6_:_
 for Y being TopStruct
for x being Point of Y holds MaxADSF x =  {  A where A is Subset of Y : ( A is anti-discrete &amp; x in A )  }  ;

registration
let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSF x ->  non empty ;
coherence
 not MaxADSF x is empty
proofend;
end;

theorem Th10: :: TEX_4:10
for Y being non empty TopStruct
for x being Point of Y holds MaxADSF x is anti-discrete-set-family
proofend;

theorem Th11: :: TEX_4:11
for Y being non empty TopStruct
for x being Point of Y holds {x} = meet (MaxADSF x)
proofend;

theorem Th12: :: TEX_4:12
for Y being non empty TopStruct
for x being Point of Y holds {x} c= union (MaxADSF x)
proofend;

theorem Th13: :: TEX_4:13
for Y being non empty TopStruct
for x being Point of Y holds union (MaxADSF x) is anti-discrete
proofend;

begin

:: 3. Maximal Anti-discrete Subsets of Topological Structures.
definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is maximal_anti-discrete  means :Def7: :: TEX_4:def 7
( IT is anti-discrete &amp; ( for D being Subset of Y st D is anti-discrete &amp; IT c= D holds
IT = D ) );
end;

:: deftheorem Def7 defines maximal_anti-discrete TEX_4:def_7_:_
 for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_anti-discrete iff ( IT is anti-discrete &amp; ( for D being Subset of Y st D is anti-discrete &amp; IT c= D holds
IT = D ) ) );

theorem :: TEX_4:14
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) &amp; D0 = D1 &amp; D0 is maximal_anti-discrete holds
D1 is maximal_anti-discrete
proofend;

theorem Th15: :: TEX_4:15
for Y being non empty TopStruct
for A being empty Subset of Y holds not A is maximal_anti-discrete
proofend;

theorem Th16: :: TEX_4:16
for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete &amp; A is open holds
A is maximal_anti-discrete
proofend;

theorem Th17: :: TEX_4:17
for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete &amp; A is closed holds
A is maximal_anti-discrete
proofend;

definition
let Y be TopStruct ;
let x be Point of Y;
func MaxADSet x ->  Subset of Y equals :: TEX_4:def 8
 union (MaxADSF x);
coherence
 union (MaxADSF x) is Subset of Y ;
end;

:: deftheorem  defines MaxADSet TEX_4:def_8_:_
 for Y being TopStruct
for x being Point of Y holds MaxADSet x = union (MaxADSF x);

registration
let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSet x ->  non empty ;
coherence
 not MaxADSet x is empty
proofend;
end;

theorem :: TEX_4:18
for Y being non empty TopStruct
for x being Point of Y holds {x} c= MaxADSet x by Th12;

theorem Th19: :: TEX_4:19
for Y being non empty TopStruct
for D being Subset of Y
for x being Point of Y st D is anti-discrete &amp; x in D holds
D c= MaxADSet x
proofend;

theorem Th20: :: TEX_4:20
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x is maximal_anti-discrete
proofend;

theorem Th21: :: TEX_4:21
for Y being non empty TopStruct
for x, y being Point of Y holds
( y in MaxADSet x iff MaxADSet y = MaxADSet x )
proofend;

theorem Th22: :: TEX_4:22
for Y being non empty TopStruct
for x, y being Point of Y holds
( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )
proofend;

theorem Th23: :: TEX_4:23
for Y being non empty TopStruct
for F being Subset of Y
for x being Point of Y st F is closed &amp; x in F holds
MaxADSet x c= F
proofend;

theorem Th24: :: TEX_4:24
for Y being non empty TopStruct
for G being Subset of Y
for x being Point of Y st G is open &amp; x in G holds
MaxADSet x c= G
proofend;

theorem :: TEX_4:25
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x c= meet  {  F where F is Subset of Y : ( F is closed &amp; x in F )  }
proofend;

theorem :: TEX_4:26
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x c= meet  {  G where G is Subset of Y : ( G is open &amp; x in G )  }
proofend;

definition
let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is maximal_anti-discrete  means :Def9: :: TEX_4:def 9
 ex x being Point of Y st
( x in A &amp; A = MaxADSet x );
compatibility
 ( A is maximal_anti-discrete iff ex x being Point of Y st
( x in A &amp; A = MaxADSet x ) )
proofend;
end;

:: deftheorem Def9 defines maximal_anti-discrete TEX_4:def_9_:_
 for Y being non empty TopStruct
for A being Subset of Y holds
( A is maximal_anti-discrete iff ex x being Point of Y st
( x in A &amp; A = MaxADSet x ) );

theorem Th27: :: TEX_4:27
for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st x in A &amp; A is maximal_anti-discrete holds
A = MaxADSet x
proofend;

definition
let Y be non empty TopStruct ;
let A be non empty Subset of Y;
redefine attr A is maximal_anti-discrete  means :: TEX_4:def 10
 for x being Point of Y st x in A holds
A = MaxADSet x;
compatibility
 ( A is maximal_anti-discrete iff for x being Point of Y st x in A holds
A = MaxADSet x )
proofend;
end;

:: deftheorem  defines maximal_anti-discrete TEX_4:def_10_:_
 for Y being non empty TopStruct
for A being non empty Subset of Y holds
( A is maximal_anti-discrete iff for x being Point of Y st x in A holds
A = MaxADSet x );

definition
let Y be non empty TopStruct ;
let A be Subset of Y;
func MaxADSet A ->  Subset of Y equals :: TEX_4:def 11
 union  {  (MaxADSet a) where a is Point of Y : a in A  }  ;
coherence
 union  {  (MaxADSet a) where a is Point of Y : a in A  }  is Subset of Y
proofend;
end;

:: deftheorem  defines MaxADSet TEX_4:def_11_:_
 for Y being non empty TopStruct
for A being Subset of Y holds MaxADSet A = union  {  (MaxADSet a) where a is Point of Y : a in A  }  ;

theorem Th28: :: TEX_4:28
for Y being non empty TopStruct
for x being Point of Y holds MaxADSet x = MaxADSet {x}
proofend;

theorem Th29: :: TEX_4:29
for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x meets A
proofend;

theorem Th30: :: TEX_4:30
for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A
proofend;

theorem Th31: :: TEX_4:31
for Y being non empty TopStruct
for A, B being Subset of Y st A c= B holds
MaxADSet A c= MaxADSet B
proofend;

theorem Th32: :: TEX_4:32
for Y being non empty TopStruct
for A being Subset of Y holds A c= MaxADSet A
proofend;

theorem Th33: :: TEX_4:33
for Y being non empty TopStruct
for A being Subset of Y holds MaxADSet A = MaxADSet (MaxADSet A)
proofend;

theorem Th34: :: TEX_4:34
for Y being non empty TopStruct
for A, B being Subset of Y st A c= MaxADSet B holds
MaxADSet A c= MaxADSet B
proofend;

theorem Th35: :: TEX_4:35
for Y being non empty TopStruct
for A, B being Subset of Y st B c= MaxADSet A &amp; A c= MaxADSet B holds
MaxADSet A = MaxADSet B
proofend;

theorem :: TEX_4:36
for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)
proofend;

theorem Th37: :: TEX_4:37
for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)
proofend;

registration
let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster MaxADSet A ->  non empty ;
coherence
 not MaxADSet A is empty by Th32, XBOOLE_1:3;
end;

registration
let Y be non empty TopStruct ;
let A be empty Subset of Y;
cluster MaxADSet A ->  empty ;
coherence
 MaxADSet A is empty
proofend;
end;

registration
let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster MaxADSet A ->  non proper ;
coherence
 not MaxADSet A is proper
proofend;
end;

registration
let Y be non trivial TopStruct ;
let A be non trivial Subset of Y;
cluster MaxADSet A ->  non trivial ;
coherence
 not MaxADSet A is trivial
proofend;
end;

theorem Th38: :: TEX_4:38
for Y being non empty TopStruct
for G, A being Subset of Y st G is open &amp; A c= G holds
MaxADSet A c= G
proofend;

theorem Th39: :: TEX_4:39
for Y being non empty TopStruct
for A being Subset of Y st  {  G where G is Subset of Y : ( G is open &amp; A c= G )  }  <> {} holds
MaxADSet A c= meet  {  G where G is Subset of Y : ( G is open &amp; A c= G )  }
proofend;

theorem Th40: :: TEX_4:40
for Y being non empty TopStruct
for F, A being Subset of Y st F is closed &amp; A c= F holds
MaxADSet A c= F
proofend;

theorem Th41: :: TEX_4:41
for Y being non empty TopStruct
for A being Subset of Y st  {  F where F is Subset of Y : ( F is closed &amp; A c= F )  }  <> {} holds
MaxADSet A c= meet  {  F where F is Subset of Y : ( F is closed &amp; A c= F )  }
proofend;

begin

:: 4. Anti-discrete and Maximal Anti-discrete Subsets of Topological Spaces.
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete  means :Def12: :: TEX_4:def 12
 for x being Point of X st x in A holds
A c= Cl {x};
compatibility
 ( A is anti-discrete iff for x being Point of X st x in A holds
A c= Cl {x} )
proofend;
end;

:: deftheorem Def12 defines anti-discrete TEX_4:def_12_:_
 for X being non empty TopSpace
for A being Subset of X holds
( A is anti-discrete iff for x being Point of X st x in A holds
A c= Cl {x} );

definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete  means :: TEX_4:def 13
 for x being Point of X st x in A holds
Cl A = Cl {x};
compatibility
 ( A is anti-discrete iff for x being Point of X st x in A holds
Cl A = Cl {x} )
proofend;
end;

:: deftheorem  defines anti-discrete TEX_4:def_13_:_
 for X being non empty TopSpace
for A being Subset of X holds
( A is anti-discrete iff for x being Point of X st x in A holds
Cl A = Cl {x} );

definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete  means :Def14: :: TEX_4:def 14
 for x, y being Point of X st x in A &amp; y in A holds
Cl {x} = Cl {y};
compatibility
 ( A is anti-discrete iff for x, y being Point of X st x in A &amp; y in A holds
Cl {x} = Cl {y} )
proofend;
end;

:: deftheorem Def14 defines anti-discrete TEX_4:def_14_:_
 for X being non empty TopSpace
for A being Subset of X holds
( A is anti-discrete iff for x, y being Point of X st x in A &amp; y in A holds
Cl {x} = Cl {y} );

theorem :: TEX_4:42
for X being non empty TopSpace
for x being Point of X
for D being Subset of X st D is anti-discrete &amp; Cl {x} c= D holds
D = Cl {x}
proofend;

theorem :: TEX_4:43
for X being non empty TopSpace
for A being Subset of X holds
( ( A is anti-discrete &amp; A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )
proofend;

theorem :: TEX_4:44
for X being non empty TopSpace
for A being Subset of X st A is anti-discrete &amp; not A is open holds
A is boundary
proofend;

theorem Th45: :: TEX_4:45
for X being non empty TopSpace
for x being Point of X st Cl {x} = {x} holds
{x} is maximal_anti-discrete
proofend;

theorem Th46: :: TEX_4:46
for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= meet  {  G where G is Subset of X : ( G is open &amp; x in G )  }
proofend;

theorem Th47: :: TEX_4:47
for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= meet  {  F where F is Subset of X : ( F is closed &amp; x in F )  }
proofend;

theorem Th48: :: TEX_4:48
for X being non empty TopSpace
for x being Point of X holds MaxADSet x c= Cl {x}
proofend;

Lm1:  for X being non empty TopSpace
for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
proofend;

theorem Th49: :: TEX_4:49
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )
proofend;

theorem :: TEX_4:50
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} )
proofend;

definition
let X be non empty TopSpace;
let x be Point of X;
:: original:MaxADSet
redefine func MaxADSet x ->  non empty Subset of X equals :: TEX_4:def 15
(Cl {x}) /\ (meet  {  G where G is Subset of X : ( G is open &amp; x in G )  }  );
compatibility
 for b1 being non empty Subset of X holds
( b1 = MaxADSet x iff b1 = (Cl {x}) /\ (meet  {  G where G is Subset of X : ( G is open &amp; x in G )  }  ) )
proofend;
coherence
 MaxADSet x is non empty Subset of X ;
end;

:: deftheorem  defines MaxADSet TEX_4:def_15_:_
 for X being non empty TopSpace
for x being Point of X holds MaxADSet x = (Cl {x}) /\ (meet  {  G where G is Subset of X : ( G is open &amp; x in G )  }  );

theorem Th51: :: TEX_4:51
for X being non empty TopSpace
for x, y being Point of X holds
( Cl {x} c= Cl {y} iff meet  {  G where G is Subset of X : ( G is open &amp; y in G )  }  c= meet  {  G where G is Subset of X : ( G is open &amp; x in G )  }  )
proofend;

theorem :: TEX_4:52
for X being non empty TopSpace
for x, y being Point of X holds
( Cl {x} c= Cl {y} iff MaxADSet y c= meet  {  G where G is Subset of X : ( G is open &amp; x in G )  }  )
proofend;

theorem Th53: :: TEX_4:53
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open &amp; MaxADSet x c= V &amp; V misses MaxADSet y ) or ex W being Subset of X st
( W is open &amp; W misses MaxADSet x &amp; MaxADSet y c= W ) ) )
proofend;

theorem :: TEX_4:54
for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st
( E is closed &amp; MaxADSet x c= E &amp; E misses MaxADSet y ) or ex F being Subset of X st
( F is closed &amp; F misses MaxADSet x &amp; MaxADSet y c= F ) ) )
proofend;

theorem Th55: :: TEX_4:55
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet  {  G where G is Subset of X : ( G is open &amp; A c= G )  }
proofend;

theorem Th56: :: TEX_4:56
for X being non empty TopSpace
for P being Subset of X st P is open holds
MaxADSet P = P
proofend;

theorem :: TEX_4:57
for X being non empty TopSpace
for A being Subset of X holds MaxADSet (Int A) = Int A by Th56;

theorem Th58: :: TEX_4:58
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= meet  {  F where F is Subset of X : ( F is closed &amp; A c= F )  }
proofend;

theorem Th59: :: TEX_4:59
for X being non empty TopSpace
for A being Subset of X holds MaxADSet A c= Cl A
proofend;

theorem Th60: :: TEX_4:60
for X being non empty TopSpace
for P being Subset of X st P is closed holds
MaxADSet P = P
proofend;

theorem :: TEX_4:61
for X being non empty TopSpace
for A being Subset of X holds MaxADSet (Cl A) = Cl A by Th60;

theorem :: TEX_4:62
for X being non empty TopSpace
for A being Subset of X holds Cl (MaxADSet A) = Cl A
proofend;

theorem :: TEX_4:63
for X being non empty TopSpace
for A, B being Subset of X st MaxADSet A = MaxADSet B holds
Cl A = Cl B
proofend;

theorem :: TEX_4:64
for X being non empty TopSpace
for P, Q being Subset of X st ( P is closed or Q is closed ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
proofend;

theorem :: TEX_4:65
for X being non empty TopSpace
for P, Q being Subset of X st ( P is open or Q is open ) holds
MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)
proofend;

begin

theorem Th66: :: TEX_4:66
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 &amp; Y0 is anti-discrete holds
A is anti-discrete
proofend;

theorem Th67: :: TEX_4:67
for Y being non empty TopStruct
for Y0 being SubSpace of Y st Y0 is TopSpace-like holds
for A being Subset of Y st A = the carrier of Y0 &amp; A is anti-discrete holds
Y0 is anti-discrete
proofend;

theorem :: TEX_4:68
for X being non empty TopSpace
for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
proofend;

theorem :: TEX_4:69
for X being non empty TopSpace
for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds
Y0 is anti-discrete
proofend;

theorem :: TEX_4:70
for X being non empty TopSpace
for Y0 being anti-discrete SubSpace of X
for X0 being open SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
proofend;

theorem :: TEX_4:71
for X being non empty TopSpace
for Y0 being anti-discrete SubSpace of X
for X0 being closed SubSpace of X holds
( Y0 misses X0 or Y0 is SubSpace of X0 )
proofend;

definition
let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attrIT is maximal_anti-discrete  means :Def16: :: TEX_4:def 16
( IT is anti-discrete &amp; ( for Y0 being SubSpace of Y st Y0 is anti-discrete &amp; the carrier of IT c= the carrier of Y0 holds
the carrier of IT = the carrier of Y0 ) );
end;

:: deftheorem Def16 defines maximal_anti-discrete TEX_4:def_16_:_
 for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_anti-discrete iff ( IT is anti-discrete &amp; ( for Y0 being SubSpace of Y st Y0 is anti-discrete &amp; the carrier of IT c= the carrier of Y0 holds
the carrier of IT = the carrier of Y0 ) ) );

registration
let Y be non empty TopStruct ;
cluster maximal_anti-discrete  ->  anti-discrete for SubSpace of Y;
coherence
 for b1 being SubSpace of Y st b1 is maximal_anti-discrete holds
b1 is anti-discrete by Def16;
cluster non anti-discrete  ->  non maximal_anti-discrete for SubSpace of Y;
coherence
 for b1 being SubSpace of Y st not b1 is anti-discrete holds
not b1 is maximal_anti-discrete ;
end;

theorem Th72: :: TEX_4:72
for X being non empty TopSpace
for Y0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
proofend;

registration
let X be non empty TopSpace;
cluster non empty open anti-discrete  ->  non empty maximal_anti-discrete for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is open &amp; b1 is anti-discrete holds
b1 is maximal_anti-discrete
proofend;
cluster non empty open non maximal_anti-discrete  ->  non empty non anti-discrete for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is open &amp; not b1 is maximal_anti-discrete holds
not b1 is anti-discrete ;
cluster non empty anti-discrete non maximal_anti-discrete  ->  non empty non open for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is anti-discrete &amp; not b1 is maximal_anti-discrete holds
not b1 is open ;
cluster non empty closed anti-discrete  ->  non empty maximal_anti-discrete for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is closed &amp; b1 is anti-discrete holds
b1 is maximal_anti-discrete
proofend;
cluster non empty closed non maximal_anti-discrete  ->  non empty non anti-discrete for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is closed &amp; not b1 is maximal_anti-discrete holds
not b1 is anti-discrete ;
cluster non empty anti-discrete non maximal_anti-discrete  ->  non empty non closed for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is anti-discrete &amp; not b1 is maximal_anti-discrete holds
not b1 is closed ;
end;

definition
let Y be TopStruct ;
let x be Point of Y;
func MaxADSspace x ->  strict SubSpace of Y means :Def17: :: TEX_4:def 17
 the carrier of it = MaxADSet x;
existence
 ex b1 being strict SubSpace of Y st the carrier of b1 = MaxADSet x
proofend;
uniqueness
 for b1, b2 being strict SubSpace of Y st the carrier of b1 = MaxADSet x &amp; the carrier of b2 = MaxADSet x holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines MaxADSspace TEX_4:def_17_:_
 for Y being TopStruct
for x being Point of Y
for b3 being strict SubSpace of Y holds
( b3 = MaxADSspace x iff the carrier of b3 = MaxADSet x );

registration
let Y be non empty TopStruct ;
let x be Point of Y;
cluster MaxADSspace x ->  non empty strict ;
coherence
 not MaxADSspace x is empty
proofend;
end;

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
proofend;

theorem :: TEX_4:73
for Y being non empty TopStruct
for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x
proofend;

theorem :: TEX_4:74
for Y being non empty TopStruct
for x, y being Point of Y holds
( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )
proofend;

theorem :: TEX_4:75
for Y being non empty TopStruct
for x, y being Point of Y holds
( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )
proofend;

registration
let X be non empty TopSpace;
cluster strict TopSpace-like maximal_anti-discrete for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is maximal_anti-discrete &amp; b1 is strict )
proofend;
end;

registration
let X be non empty TopSpace;
let x be Point of X;
cluster MaxADSspace x ->  strict maximal_anti-discrete ;
coherence
 MaxADSspace x is maximal_anti-discrete
proofend;
end;

theorem :: TEX_4:76
for X being non empty TopSpace
for X0 being non empty closed SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
proofend;

theorem :: TEX_4:77
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0
proofend;

theorem :: TEX_4:78
for X being non empty TopSpace
for x being Point of X st Cl {x} = {x} holds
Sspace x is maximal_anti-discrete
proofend;

notation
let Y be TopStruct ;
let A be Subset of Y;
synonym  Sspace A for Y | A;
end;

Lm3:  for Y being TopStruct
for A being Subset of Y holds the carrier of (Y | A) = A
proofend;

theorem :: TEX_4:79
for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (Sspace A)
proofend;

theorem :: TEX_4:80
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0
proofend;

registration
let Y be non trivial TopStruct ;
cluster strict non proper for SubSpace of Y;
existence
 ex b1 being SubSpace of Y st
( not b1 is proper &amp; b1 is strict )
proofend;
end;

registration
let Y be non trivial TopStruct ;
let A be non trivial Subset of Y;
cluster Sspace A ->  non trivial ;
coherence
 not Sspace A is trivial by Lm3;
end;

registration
let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster Sspace A ->  non proper ;
coherence
 not Sspace A is proper
proofend;
end;

definition
let Y be non empty TopStruct ;
let A be Subset of Y;
func MaxADSspace A ->  strict SubSpace of Y means :Def18: :: TEX_4:def 18
 the carrier of it = MaxADSet A;
existence
 ex b1 being strict SubSpace of Y st the carrier of b1 = MaxADSet A
proofend;
uniqueness
 for b1, b2 being strict SubSpace of Y st the carrier of b1 = MaxADSet A &amp; the carrier of b2 = MaxADSet A holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines MaxADSspace TEX_4:def_18_:_
 for Y being non empty TopStruct
for A being Subset of Y
for b3 being strict SubSpace of Y holds
( b3 = MaxADSspace A iff the carrier of b3 = MaxADSet A );

registration
let Y be non empty TopStruct ;
let A be non empty Subset of Y;
cluster MaxADSspace A ->  non empty strict ;
coherence
 not MaxADSspace A is empty
proofend;
end;

theorem :: TEX_4:81
for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)
proofend;

theorem :: TEX_4:82
for Y being non empty TopStruct
for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A
proofend;

theorem :: TEX_4:83
for Y being non empty TopStruct
for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #)
proofend;

theorem :: TEX_4:84
for Y being non empty TopStruct
for A, B being non empty Subset of Y st A c= B holds
MaxADSspace A is SubSpace of MaxADSspace B
proofend;

theorem :: TEX_4:85
for Y being non empty TopStruct
for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)
proofend;

theorem :: TEX_4:86
for Y being non empty TopStruct
for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds
MaxADSspace A is SubSpace of MaxADSspace B
proofend;

theorem :: TEX_4:87
for Y being non empty TopStruct
for A, B being non empty Subset of Y holds
( ( B is Subset of (MaxADSspace A) &amp; A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) )
proofend;

registration
let Y be non trivial TopStruct ;
let A be non trivial Subset of Y;
cluster MaxADSspace A ->  non trivial strict ;
coherence
 not MaxADSspace A is trivial
proofend;
end;

registration
let Y be non empty TopStruct ;
let A be non proper Subset of Y;
cluster MaxADSspace A ->  strict non proper ;
coherence
 not MaxADSspace A is proper
proofend;
end;

theorem :: TEX_4:88
for X being non empty TopSpace
for X0 being open SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
proofend;

theorem :: TEX_4:89
for X being non empty TopSpace
for X0 being closed SubSpace of X
for A being non empty Subset of X st A is Subset of X0 holds
MaxADSspace A is SubSpace of X0
proofend;