:: TDLAT_3 semantic presentation

begin

theorem :: TDLAT_3:1
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for C being ( ( ) ( ) Subset of ) holds Cl C : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = (Int (C : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:2
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for C being ( ( ) ( ) Subset of ) holds Cl (C : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = (Int C : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:3
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for C being ( ( ) ( ) Subset of ) holds Int (C : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = (Cl C : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:4
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) & A : ( ( ) ( ) Subset of ) is closed holds
A : ( ( ) ( ) Subset of ) \/ (Int B : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ;

theorem :: TDLAT_3:5
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds
( ( A : ( ( ) ( ) Subset of ) is open & A : ( ( ) ( ) Subset of ) is closed ) iff Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:6
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open & A : ( ( ) ( ) Subset of ) is closed holds
Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:7
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed & Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ) is open_condensed & A : ( ( ) ( ) Subset of ) is closed_condensed ) ;

theorem :: TDLAT_3:8
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed & Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ) is open & A : ( ( ) ( ) Subset of ) is closed ) ;

theorem :: TDLAT_3:9
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
( Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let IT be ( ( ) ( ) TopStruct ) ;
attr IT is discrete means :: TDLAT_3:def 1
 the topology of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) Element of K10(K10( the carrier of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = bool the carrier of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10( the carrier of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
attr IT is anti-discrete means :: TDLAT_3:def 2
 the topology of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) Element of K10(K10( the carrier of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( empty ) set ) , the carrier of IT : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;
end;

theorem :: TDLAT_3:10
for Y being ( ( ) ( ) TopStruct ) st Y : ( ( ) ( ) TopStruct ) is discrete & Y : ( ( ) ( ) TopStruct ) is anti-discrete holds
bool the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( empty ) set ) , the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) ;

theorem :: TDLAT_3:11
for Y being ( ( ) ( ) TopStruct ) st {} : ( ( ) ( empty ) set ) in the topology of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) in the topology of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & bool the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( empty ) set ) , the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
( Y : ( ( ) ( ) TopStruct ) is discrete & Y : ( ( ) ( ) TopStruct ) is anti-discrete ) ;

registration
cluster non empty strict discrete anti-discrete for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TDLAT_3:12
for Y being ( ( discrete ) ( discrete ) TopStruct )
for A being ( ( ) ( ) Subset of ) holds the carrier of Y : ( ( discrete ) ( discrete ) TopStruct ) : ( ( ) ( ) set ) \ A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( discrete ) ( discrete ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in the topology of Y : ( ( discrete ) ( discrete ) TopStruct ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( discrete ) ( discrete ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:13
for Y being ( ( anti-discrete ) ( anti-discrete ) TopStruct )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in the topology of Y : ( ( anti-discrete ) ( anti-discrete ) TopStruct ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( anti-discrete ) ( anti-discrete ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
the carrier of Y : ( ( anti-discrete ) ( anti-discrete ) TopStruct ) : ( ( ) ( ) set ) \ A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( anti-discrete ) ( anti-discrete ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) in the topology of Y : ( ( anti-discrete ) ( anti-discrete ) TopStruct ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( anti-discrete ) ( anti-discrete ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

registration
cluster discrete -> TopSpace-like for ( ( ) ( ) TopStruct ) ;
cluster anti-discrete -> TopSpace-like for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TDLAT_3:14
for Y being ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) st bool the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( empty ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) holds
( Y : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) is discrete & Y : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) is anti-discrete ) ;

definition
let IT be ( ( ) ( ) TopStruct ) ;
attr IT is almost_discrete means :: TDLAT_3:def 3
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in the topology of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of K10(K10( the carrier of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
the carrier of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) \ A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) in the topology of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of K10(K10( the carrier of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster discrete -> almost_discrete for ( ( ) ( ) TopStruct ) ;
cluster anti-discrete -> almost_discrete for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster strict almost_discrete for ( ( ) ( ) TopStruct ) ;
end;

begin

registration
cluster non empty strict TopSpace-like discrete anti-discrete for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TDLAT_3:15
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is discrete iff for A being ( ( ) ( ) Subset of ) holds A : ( ( ) ( ) Subset of ) is open ) ;

theorem :: TDLAT_3:16
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is discrete iff for A being ( ( ) ( ) Subset of ) holds A : ( ( ) ( ) Subset of ) is closed ) ;

theorem :: TDLAT_3:17
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st ( for A being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) holds
A : ( ( ) ( ) Subset of ) is open ) holds
X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is discrete ;

registration
let X be ( ( non empty TopSpace-like discrete ) ( non empty TopSpace-like discrete almost_discrete ) TopSpace) ;
cluster -> closed open discrete for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like discrete ) ( non empty TopSpace-like discrete almost_discrete ) TopSpace) ;
cluster strict TopSpace-like closed open discrete almost_discrete for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like discrete ) ( non empty TopSpace-like discrete almost_discrete ) TopStruct ) ) ;
end;

theorem :: TDLAT_3:18
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is anti-discrete iff for A being ( ( ) ( ) Subset of ) holds
( not A : ( ( ) ( ) Subset of ) is open or A : ( ( ) ( ) Subset of ) = {} : ( ( ) ( empty ) set ) or A : ( ( ) ( ) Subset of ) = the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ;

theorem :: TDLAT_3:19
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is anti-discrete iff for A being ( ( ) ( ) Subset of ) holds
( not A : ( ( ) ( ) Subset of ) is closed or A : ( ( ) ( ) Subset of ) = {} : ( ( ) ( empty ) set ) or A : ( ( ) ( ) Subset of ) = the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ;

theorem :: TDLAT_3:20
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st ( for A being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) holds
X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is anti-discrete ;

registration
let X be ( ( non empty TopSpace-like anti-discrete ) ( non empty TopSpace-like anti-discrete almost_discrete ) TopSpace) ;
cluster -> anti-discrete for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like discrete ) ( non empty TopSpace-like discrete almost_discrete ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like anti-discrete ) ( non empty TopSpace-like anti-discrete almost_discrete ) TopSpace) ;
cluster TopSpace-like anti-discrete almost_discrete for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like anti-discrete ) ( non empty TopSpace-like anti-discrete almost_discrete ) TopStruct ) ) ;
end;

theorem :: TDLAT_3:21
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is almost_discrete iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
A : ( ( ) ( ) Subset of ) is closed ) ;

theorem :: TDLAT_3:22
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is almost_discrete iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed holds
A : ( ( ) ( ) Subset of ) is open ) ;

theorem :: TDLAT_3:23
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is almost_discrete iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ) ) ;

theorem :: TDLAT_3:24
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is almost_discrete iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed holds
Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ) ) ;

registration
cluster strict TopSpace-like almost_discrete for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TDLAT_3:25
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st ( for A being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) is open ) holds
X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is almost_discrete ;

theorem :: TDLAT_3:26
for X being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds
( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is discrete iff ( X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) is almost_discrete & ( for A being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) holds
A : ( ( ) ( ) Subset of ) is closed ) ) ) ;

registration
cluster TopSpace-like discrete -> TopSpace-like almost_discrete for ( ( ) ( ) TopStruct ) ;
cluster TopSpace-like anti-discrete -> TopSpace-like almost_discrete for ( ( ) ( ) TopStruct ) ;
end;

registration
let X be ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete ) TopSpace) ;
cluster non empty -> non empty almost_discrete for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like anti-discrete ) ( non empty TopSpace-like anti-discrete almost_discrete ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete ) TopSpace) ;
cluster open -> closed for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like anti-discrete ) ( non empty TopSpace-like anti-discrete almost_discrete ) TopStruct ) ) ;
cluster closed -> open for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like anti-discrete ) ( non empty TopSpace-like anti-discrete almost_discrete ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete ) TopSpace) ;
cluster non empty strict TopSpace-like almost_discrete for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete ) TopStruct ) ) ;
end;

begin

definition
let IT be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
attr IT is extremally_disconnected means :: TDLAT_3:def 4
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of IT : ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is open ;
end;

registration
cluster non empty strict TopSpace-like extremally_disconnected for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TDLAT_3:27
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed holds
Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is closed ) ;

theorem :: TDLAT_3:28
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open & B : ( ( ) ( ) Subset of ) is open & A : ( ( ) ( ) Subset of ) misses B : ( ( ) ( ) Subset of ) holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) misses Cl B : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:29
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed & B : ( ( ) ( ) Subset of ) is closed & A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) holds
(Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (Int B : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:30
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:31
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed holds
Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:32
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
( A : ( ( ) ( ) Subset of ) is closed & A : ( ( ) ( ) Subset of ) is open ) ) ;

theorem :: TDLAT_3:33
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
( A : ( ( ) ( ) Subset of ) is closed_condensed & A : ( ( ) ( ) Subset of ) is open_condensed ) ) ;

theorem :: TDLAT_3:34
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:35
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:36
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff for A being ( ( ) ( ) Subset of ) holds
( ( A : ( ( ) ( ) Subset of ) is open_condensed implies A : ( ( ) ( ) Subset of ) is closed_condensed ) & ( A : ( ( ) ( ) Subset of ) is closed_condensed implies A : ( ( ) ( ) Subset of ) is open_condensed ) ) ) ;

definition
let IT be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
attr IT is hereditarily_extremally_disconnected means :: TDLAT_3:def 5
 for X0 being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of IT : ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete ) TopStruct ) ) holds X0 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of IT : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is extremally_disconnected ;
end;

registration
cluster non empty strict TopSpace-like hereditarily_extremally_disconnected for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like hereditarily_extremally_disconnected -> non empty TopSpace-like extremally_disconnected for ( ( ) ( ) TopStruct ) ;
cluster non empty TopSpace-like almost_discrete -> non empty TopSpace-like hereditarily_extremally_disconnected for ( ( ) ( ) TopStruct ) ;
end;

theorem :: TDLAT_3:37
for X being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace)
for X0 being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of X0 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( non empty ) set ) & A : ( ( ) ( ) Subset of ) is dense holds
X0 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) is extremally_disconnected ;

registration
let X be ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ;
cluster non empty open -> non empty extremally_disconnected for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like almost_discrete ) ( non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ;
cluster non empty strict TopSpace-like extremally_disconnected for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like hereditarily_extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected hereditarily_extremally_disconnected ) TopSpace) ;
cluster non empty -> non empty hereditarily_extremally_disconnected for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopStruct ) ) ;
end;

registration
let X be ( ( non empty TopSpace-like hereditarily_extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected hereditarily_extremally_disconnected ) TopSpace) ;
cluster non empty strict TopSpace-like extremally_disconnected hereditarily_extremally_disconnected for ( ( ) ( ) SubSpace of X : ( ( non empty TopSpace-like hereditarily_extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected hereditarily_extremally_disconnected ) TopStruct ) ) ;
end;

theorem :: TDLAT_3:38
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st ( for X0 being ( ( non empty closed ) ( non empty TopSpace-like closed ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds X0 : ( ( non empty closed ) ( non empty TopSpace-like closed ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is extremally_disconnected ) holds
X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is hereditarily_extremally_disconnected ;

begin

theorem :: TDLAT_3:39
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) holds Domains_of Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Closed_Domains_of Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:40
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) holds
( D-Union Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = CLD-Union Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & D-Meet Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = CLD-Meet Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Closed_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:41
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) holds Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) = Closed_Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean ) LattStr ) ;

theorem :: TDLAT_3:42
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) holds Domains_of Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = Open_Domains_of Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:43
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) holds
( D-Union Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = OPD-Union Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & D-Meet Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = OPD-Meet Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( V12() V21(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Open_Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_3:44
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) holds Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) = Open_Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean ) LattStr ) ;

theorem :: TDLAT_3:45
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace)
for A, B being ( ( ) ( ) Element of Domains_of Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
( (D-Union Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . (A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) = A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) \/ B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & (D-Meet Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) V11( Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) V12() V21(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) , Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K10(K11(K11((Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ,(Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . (A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) = A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) /\ B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: TDLAT_3:46
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A, B being ( ( ) ( ) Element of Domains_of Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Domains_Lattice b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) \/ B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Domains_Lattice b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) /\ B : ( ( ) ( ) Element of Domains_of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( ) Element of K10(K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: TDLAT_3:47
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace)
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is domains-family holds
for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) = F : ( ( ) ( ) Subset-Family of ) holds
"\/" (S : ( ( ) ( ) Subset of ) ,(Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (Domains_Lattice b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) : ( ( ) ( non empty ) set ) ) = Cl (union F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_3:48
for Y being ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace)
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is domains-family holds
for S being ( ( ) ( ) Subset of ) st S : ( ( ) ( ) Subset of ) = F : ( ( ) ( ) Subset-Family of ) holds
( ( S : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty ) set ) implies "/\" (S : ( ( ) ( ) Subset of ) ,(Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (Domains_Lattice b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) : ( ( ) ( non empty ) set ) ) = Int (meet F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) & ( S : ( ( ) ( ) Subset of ) = {} : ( ( ) ( empty ) set ) implies "/\" (S : ( ( ) ( ) Subset of ) ,(Domains_Lattice Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (Domains_Lattice b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) ) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) : ( ( ) ( non empty ) set ) ) = [#] Y : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like extremally_disconnected ) ( non empty TopSpace-like extremally_disconnected ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: TDLAT_3:49
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff Domains_Lattice X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) is ( ( non empty Lattice-like modular ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular ) M_Lattice) ) ;

theorem :: TDLAT_3:50
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st Domains_Lattice X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) = Closed_Domains_Lattice X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean ) LattStr ) holds
X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected ;

theorem :: TDLAT_3:51
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st Domains_Lattice X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) = Open_Domains_Lattice X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean ) LattStr ) holds
X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected ;

theorem :: TDLAT_3:52
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected ;

theorem :: TDLAT_3:53
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is extremally_disconnected iff Domains_Lattice X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( non empty Lattice-like V112() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented ) LattStr ) is ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean ) B_Lattice) ) ;