:: TDLAT_1 semantic presentation

begin

theorem :: TDLAT_1:1
for T being ( ( ) ( ) 1-sorted )
for A, B being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff A : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ) ) ;

theorem :: TDLAT_1:2
for T being ( ( ) ( ) 1-sorted )
for A, B being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) misses B : ( ( ) ( ) Subset of ) iff B : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: TDLAT_1:3
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Cl (Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:4
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= Int (Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:5
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Int (Cl (Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:6
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st ( A : ( ( ) ( ) Subset of ) is closed or B : ( ( ) ( ) Subset of ) is closed ) holds
(Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (Cl (Int B : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Cl (Int (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:7
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st ( A : ( ( ) ( ) Subset of ) is open or B : ( ( ) ( ) Subset of ) is open ) holds
(Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (Int (Cl B : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Int (Cl (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:8
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Int (A : ( ( ) ( ) Subset of ) /\ (Cl (A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:9
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Cl (A : ( ( ) ( ) Subset of ) \/ (Int (A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( open closed dense ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:10
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) holds (Int (Cl (A : ( ( ) ( ) Subset of ) \/ ((Int (Cl B : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ) \/ ((Int (Cl B : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (Int (Cl (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:11
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, C being ( ( ) ( ) Subset of ) holds (Int (Cl (((Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (((Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (Int (Cl (A : ( ( ) ( ) Subset of ) \/ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ) \/ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:12
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) holds (Cl (Int (A : ( ( ) ( ) Subset of ) /\ ((Cl (Int B : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (A : ( ( ) ( ) Subset of ) /\ ((Cl (Int B : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (Cl (Int (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:13
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, C being ( ( ) ( ) Subset of ) holds (Cl (Int (((Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (((Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (Cl (Int (A : ( ( ) ( ) Subset of ) /\ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (A : ( ( ) ( ) Subset of ) /\ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: TDLAT_1:14
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds {} T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is condensed ;

theorem :: TDLAT_1:15
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds [#] T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( open closed dense ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is condensed ;

theorem :: TDLAT_1:16
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
A : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is condensed ;

theorem :: TDLAT_1:17
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed & B : ( ( ) ( ) Subset of ) is condensed holds
( (Int (Cl (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is condensed & (Cl (Int (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is condensed ) ;

theorem :: TDLAT_1:18
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds {} T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed_condensed ;

theorem :: TDLAT_1:19
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds [#] T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( open closed dense ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed_condensed ;

theorem :: TDLAT_1:20
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds {} T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open_condensed ;

theorem :: TDLAT_1:21
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds [#] T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( open closed dense ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open_condensed ;

theorem :: TDLAT_1:22
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Cl (Int A : ( ( ) ( ) Subset of ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed_condensed ;

theorem :: TDLAT_1:23
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) holds Int (Cl A : ( ( ) ( ) Subset of ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open_condensed ;

theorem :: TDLAT_1:24
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
Cl A : ( ( ) ( ) Subset of ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed_condensed ;

theorem :: TDLAT_1:25
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
Int A : ( ( ) ( ) Subset of ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open_condensed ;

theorem :: TDLAT_1:26
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
Cl (A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is closed_condensed ;

theorem :: TDLAT_1:27
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is condensed holds
Int (A : ( ( ) ( ) Subset of ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is open_condensed ;

theorem :: TDLAT_1:28
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B, C being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed_condensed & B : ( ( ) ( ) Subset of ) is closed_condensed & C : ( ( ) ( ) Subset of ) is closed_condensed holds
Cl (Int (A : ( ( ) ( ) Subset of ) /\ (Cl (Int (B : ( ( ) ( ) Subset of ) /\ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Cl (Int ((Cl (Int (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TDLAT_1:29
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B, C being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open_condensed & B : ( ( ) ( ) Subset of ) is open_condensed & C : ( ( ) ( ) Subset of ) is open_condensed holds
Int (Cl (A : ( ( ) ( ) Subset of ) \/ (Int (Cl (B : ( ( ) ( ) Subset of ) \/ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Int (Cl ((Int (Cl (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ C : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

definition
let T be ( ( ) ( ) TopStruct ) ;
func Domains_of T -> ( ( ) ( ) Subset-Family of ) equals :: TDLAT_1:def 1
 { A : ( ( ) ( ) Subset of ) where A is ( ( ) ( ) Subset of ) : A : ( ( ) ( ) Subset of ) is condensed } ;
end;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) Subset-Family of ) -> non empty ;
end;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Domains_Union T -> ( ( Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) means :: TDLAT_1:def 2
 for A, B being ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) holds it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . (A : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) = (Int (Cl (A : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) \/ B : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) \/ (A : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) \/ B : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
synonym D-Union T for Domains_Union T;
end;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Domains_Meet T -> ( ( Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) means :: TDLAT_1:def 3
 for A, B being ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) holds it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . (A : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) = (Cl (Int (A : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) /\ B : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (A : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) /\ B : ( ( ) ( ) Element of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
synonym D-Meet T for Domains_Meet T;
end;

theorem :: TDLAT_1:30
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds LattStr(# (Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(D-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,(D-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) #) : ( ( strict ) ( non empty strict ) LattStr ) is ( ( non empty Lattice-like V86() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() complemented ) C_Lattice) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Domains_Lattice T -> ( ( non empty Lattice-like V86() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() complemented ) C_Lattice) equals :: TDLAT_1:def 4
 LattStr(# (Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ,(Domains_Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) #) : ( ( strict ) ( non empty strict ) LattStr ) ;
end;

begin

definition
let T be ( ( ) ( ) TopStruct ) ;
func Closed_Domains_of T -> ( ( ) ( ) Subset-Family of ) equals :: TDLAT_1:def 5
 { A : ( ( ) ( ) Subset of ) where A is ( ( ) ( ) Subset of ) : A : ( ( ) ( ) Subset of ) is closed_condensed } ;
end;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) Subset-Family of ) -> non empty ;
end;

theorem :: TDLAT_1:31
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) c= Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Closed_Domains_Union T -> ( ( Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) means :: TDLAT_1:def 6
 for A, B being ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) holds it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . (A : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) = A : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) \/ B : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
synonym CLD-Union T for Closed_Domains_Union T;
end;

theorem :: TDLAT_1:32
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) holds (CLD-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) set ) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Closed_Domains_Meet T -> ( ( Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) means :: TDLAT_1:def 7
 for A, B being ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) holds it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . (A : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) = Cl (Int (A : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) /\ B : ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( open ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( closed ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
synonym CLD-Meet T for Closed_Domains_Meet T;
end;

theorem :: TDLAT_1:33
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Element of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) holds (CLD-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) set ) ;

theorem :: TDLAT_1:34
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds LattStr(# (Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(CLD-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,(CLD-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) #) : ( ( strict ) ( non empty strict ) 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 V86() complemented Boolean ) B_Lattice) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Closed_Domains_Lattice T -> ( ( 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 V86() complemented Boolean ) B_Lattice) equals :: TDLAT_1:def 8
 LattStr(# (Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ,(Closed_Domains_Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) #) : ( ( strict ) ( non empty strict ) LattStr ) ;
end;

begin

definition
let T be ( ( ) ( ) TopStruct ) ;
func Open_Domains_of T -> ( ( ) ( ) Subset-Family of ) equals :: TDLAT_1:def 9
 { A : ( ( ) ( ) Subset of ) where A is ( ( ) ( ) Subset of ) : A : ( ( ) ( ) Subset of ) is open_condensed } ;
end;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) Subset-Family of ) -> non empty ;
end;

theorem :: TDLAT_1:35
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) c= Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Open_Domains_Union T -> ( ( Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) means :: TDLAT_1:def 10
 for A, B being ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) holds it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . (A : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) = Int (Cl (A : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) \/ B : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( closed ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( open ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
synonym OPD-Union T for Open_Domains_Union T;
end;

theorem :: TDLAT_1:36
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) holds (OPD-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) set ) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Open_Domains_Meet T -> ( ( Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) means :: TDLAT_1:def 11
 for A, B being ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) holds it : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) . (A : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) = A : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) /\ B : ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
synonym OPD-Meet T for Open_Domains_Meet T;
end;

theorem :: TDLAT_1:37
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A, B being ( ( ) ( ) Element of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) holds (OPD-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) . (A : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,B : ( ( ) ( ) Element of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) set ) ;

theorem :: TDLAT_1:38
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds LattStr(# (Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(OPD-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ,(OPD-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) #) : ( ( strict ) ( non empty strict ) 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 V86() complemented Boolean ) B_Lattice) ;

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
func Open_Domains_Lattice T -> ( ( 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 V86() complemented Boolean ) B_Lattice) equals :: TDLAT_1:def 12
 LattStr(# (Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ,(Open_Domains_Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Subset-Family of ) ) #) : ( ( strict ) ( non empty strict ) LattStr ) ;
end;

begin

theorem :: TDLAT_1:39
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds CLD-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) || (Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) : ( ( ) ( V1() Function-like ) set ) ;

theorem :: TDLAT_1:40
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds CLD-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Closed_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) || (Closed_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) : ( ( ) ( V1() Function-like ) set ) ;

theorem :: TDLAT_1:41
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds Closed_Domains_Lattice T : ( ( TopSpace-like ) ( 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 V86() complemented Boolean ) B_Lattice) is ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of Domains_Lattice T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( non empty Lattice-like V86() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() complemented ) C_Lattice) ) ;

theorem :: TDLAT_1:42
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds OPD-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Union T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) || (Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) : ( ( ) ( V1() Function-like ) set ) ;

theorem :: TDLAT_1:43
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds OPD-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Open_Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) = (D-Meet T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) ( V1() V4([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) ) V5( Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) Function-like V18([:(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) ,(Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) :] : ( ( ) ( V1() non empty ) set ) , Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) ) BinOp of Domains_of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Subset-Family of ) ) || (Open_Domains_of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) Subset-Family of ) : ( ( ) ( V1() Function-like ) set ) ;

theorem :: TDLAT_1:44
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) holds Open_Domains_Lattice T : ( ( TopSpace-like ) ( 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 V86() complemented Boolean ) B_Lattice) is ( ( ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) SubLattice of Domains_Lattice T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( non empty Lattice-like V86() complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V86() complemented ) C_Lattice) ) ;