:: TEX_3 semantic presentation
begin
theorem
:: TEX_3:1
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) ,
B
: ( ( ) ( )
Subset
of )
constitute_a_decomposition
holds
( not
A
: ( ( ) ( )
Subset
of ) is
empty
iff
B
: ( ( ) ( )
Subset
of ) is
proper
) ;
theorem
:: TEX_3:2
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) ,
B
: ( ( ) ( )
Subset
of )
constitute_a_decomposition
holds
(
A
: ( ( ) ( )
Subset
of ) is
dense
iff
B
: ( ( ) ( )
Subset
of ) is
boundary
) ;
theorem
:: TEX_3:3
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) ,
B
: ( ( ) ( )
Subset
of )
constitute_a_decomposition
holds
(
A
: ( ( ) ( )
Subset
of ) is
boundary
iff
B
: ( ( ) ( )
Subset
of ) is
dense
) ;
theorem
:: TEX_3:4
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) ,
B
: ( ( ) ( )
Subset
of )
constitute_a_decomposition
holds
(
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
iff
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
) ;
theorem
:: TEX_3:5
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) ,
B
: ( ( ) ( )
Subset
of )
constitute_a_decomposition
holds
(
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
iff
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) ;
theorem
:: TEX_3:6
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y1
,
Y2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
Y1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ,
Y2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
constitute_a_decomposition
holds
(
Y1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
proper
&
Y2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
proper
) ;
theorem
:: TEX_3:7
for
X
being ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
)
for
D
being ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) ex
Y0
being ( ( non
empty
strict
proper
) ( non
empty
strict
TopSpace-like
proper
)
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) st
D
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of )
=
the
carrier
of
Y0
: ( ( non
empty
strict
proper
) ( non
empty
strict
TopSpace-like
proper
)
SubSpace
of
b
1
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TEX_3:8
for
X
being ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
)
for
Y1
being ( ( non
empty
proper
) ( non
empty
TopSpace-like
proper
)
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) ex
Y2
being ( ( non
empty
strict
proper
) ( non
empty
strict
TopSpace-like
proper
)
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) st
Y1
: ( ( non
empty
proper
) ( non
empty
TopSpace-like
proper
)
SubSpace
of
b
1
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) ,
Y2
: ( ( non
empty
strict
proper
) ( non
empty
strict
TopSpace-like
proper
)
SubSpace
of
b
1
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) )
constitute_a_decomposition
;
begin
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
IT
be ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
attr
IT
is
dense
means
:: TEX_3:def 1
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
IT
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) holds
A
: ( ( ) ( )
Subset
of ) is
dense
;
end;
theorem
:: TEX_3:9
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) holds
(
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
iff
A
: ( ( ) ( )
Subset
of ) is
dense
) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
closed
dense
->
non
proper
for ( ( ) ( )
SubSpace
of
X
: ( ( ) ( )
TopStruct
) ) ;
cluster
proper
dense
->
non
closed
for ( ( ) ( )
SubSpace
of
X
: ( ( ) ( )
TopStruct
) ) ;
cluster
closed
proper
->
non
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( ) ( )
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:10
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
dense
holds
ex
X0
being ( ( non
empty
strict
dense
) ( non
empty
strict
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
strict
dense
) ( non
empty
strict
TopSpace-like
dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TEX_3:11
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
(
B
: ( ( ) ( )
Subset
of ) is
dense
iff
A
: ( ( ) ( )
Subset
of ) is
dense
) ;
theorem
:: TEX_3:12
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X2
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
;
theorem
:: TEX_3:13
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X1
: ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
theorem
:: TEX_3:14
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X2
being ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
X1
: ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X2
: ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
b
2
: ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) is ( ( non
empty
dense
) ( non
empty
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
theorem
:: TEX_3:15
for
X
,
Y1
,
Y2
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
=
TopStruct
(# the
carrier
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) , the
topology
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) holds
(
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) iff
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
IT
be ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
attr
IT
is
everywhere_dense
means
:: TEX_3:def 2
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) holds
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
;
end;
theorem
:: TEX_3:16
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) holds
(
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
iff
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
everywhere_dense
->
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
non
dense
->
non
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
non
proper
->
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
non
everywhere_dense
->
proper
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:17
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
everywhere_dense
holds
ex
X0
being ( ( non
empty
strict
everywhere_dense
) ( non
empty
strict
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
strict
everywhere_dense
) ( non
empty
strict
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TEX_3:18
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
(
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
iff
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) ;
theorem
:: TEX_3:19
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X2
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
;
theorem
:: TEX_3:20
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X1
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
theorem
:: TEX_3:21
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
being ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X2
being ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X1
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X2
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
2
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) is ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
theorem
:: TEX_3:22
for
X
,
Y1
,
Y2
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
=
TopStruct
(# the
carrier
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) , the
topology
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) holds
(
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) iff
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
open
dense
->
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
dense
non
everywhere_dense
->
non
open
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
open
non
everywhere_dense
->
non
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
open
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:23
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
dense
&
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
holds
ex
X0
being ( ( non
empty
strict
open
dense
) ( non
empty
strict
TopSpace-like
open
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
strict
open
dense
) ( non
empty
strict
TopSpace-like
open
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TEX_3:24
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
(
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
iff ex
X1
being ( (
strict
open
dense
) (
strict
TopSpace-like
open
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( (
strict
open
dense
) (
strict
TopSpace-like
open
dense
everywhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ) ;
theorem
:: TEX_3:25
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
or
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
) holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
union
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
theorem
:: TEX_3:26
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
or
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
) holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
union
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
theorem
:: TEX_3:27
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
&
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
meet
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( (
everywhere_dense
) (
TopSpace-like
dense
everywhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
theorem
:: TEX_3:28
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st ( (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
&
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
) or (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
&
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
) ) holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
meet
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( (
dense
) (
TopSpace-like
dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
begin
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
IT
be ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
attr
IT
is
boundary
means
:: TEX_3:def 3
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) holds
A
: ( ( ) ( )
Subset
of ) is
boundary
;
end;
theorem
:: TEX_3:29
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) holds
(
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
iff
A
: ( ( ) ( )
Subset
of ) is
boundary
) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
open
->
non
empty
non
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
non
empty
boundary
->
non
empty
non
open
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
everywhere_dense
->
non
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
boundary
->
non
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:30
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
boundary
holds
ex
X0
being ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
&
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TEX_3:31
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ,
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
constitute_a_decomposition
holds
(
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
iff
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
) ;
theorem
:: TEX_3:32
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ,
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
constitute_a_decomposition
holds
(
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
iff
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
) ;
theorem
:: TEX_3:33
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
holds
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) holds
A
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TEX_3:34
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
&
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
IT
be ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ;
attr
IT
is
nowhere_dense
means
:: TEX_3:def 4
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) holds
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
;
end;
theorem
:: TEX_3:35
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) holds
(
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
iff
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
nowhere_dense
->
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
non
boundary
->
non
nowhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
nowhere_dense
->
non
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
dense
->
non
nowhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:36
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
nowhere_dense
holds
ex
X0
being ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
&
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TEX_3:37
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ,
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
constitute_a_decomposition
holds
(
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
iff
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
) ;
theorem
:: TEX_3:38
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ,
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
constitute_a_decomposition
holds
(
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
iff
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
) ;
theorem
:: TEX_3:39
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
holds
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) holds
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
;
theorem
:: TEX_3:40
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
&
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X1
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) holds
X2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
closed
boundary
->
nowhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
boundary
non
nowhere_dense
->
non
closed
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
closed
non
nowhere_dense
->
non
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:41
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
boundary
&
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
closed
holds
ex
X0
being ( ( non
empty
strict
closed
) ( non
empty
strict
TopSpace-like
closed
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( ( non
empty
strict
closed
) ( non
empty
strict
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
&
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
strict
closed
) ( non
empty
strict
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_3:42
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
(
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
iff ex
X1
being ( ( non
empty
strict
closed
) ( non
empty
strict
TopSpace-like
closed
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X1
: ( ( non
empty
strict
closed
) ( non
empty
strict
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
&
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X1
: ( ( non
empty
strict
closed
) ( non
empty
strict
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ) ) ;
theorem
:: TEX_3:43
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
or
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
) &
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
meets
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
meet
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
;
theorem
:: TEX_3:44
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
&
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
union
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
;
theorem
:: TEX_3:45
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st ( (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
&
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
) or (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
&
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
) ) holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
union
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
;
theorem
:: TEX_3:46
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X1
,
X2
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st (
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
or
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
) &
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
meets
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
X1
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
meet
X2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
;
begin
theorem
:: TEX_3:47
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ( for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds not
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
) holds
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
discrete
;
theorem
:: TEX_3:48
for
X
being ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) st ( for
X0
being ( (
proper
) (
TopSpace-like
proper
)
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) holds not
X0
: ( (
proper
) (
TopSpace-like
proper
)
SubSpace
of
b
1
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) is
dense
) holds
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) is
discrete
;
registration
let
X
be ( ( non
empty
TopSpace-like
discrete
) ( non
empty
TopSpace-like
discrete
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopSpace
) ;
cluster
non
empty
->
non
empty
non
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
proper
->
non
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
cluster
dense
->
non
proper
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
discrete
) ( non
empty
TopSpace-like
discrete
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
closed
open
discrete
almost_discrete
non
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
discrete
) ( non
empty
TopSpace-like
discrete
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
trivial
TopSpace-like
discrete
) ( non
empty
non
trivial
TopSpace-like
discrete
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopSpace
) ;
cluster
strict
TopSpace-like
closed
open
discrete
almost_discrete
non
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
discrete
) ( non
empty
non
trivial
TopSpace-like
discrete
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:49
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ex
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
holds
not
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
discrete
;
theorem
:: TEX_3:50
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ex
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
&
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
proper
) holds
not
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
discrete
;
registration
let
X
be ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
non
empty
strict
TopSpace-like
proper
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:51
for
X
being ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
boundary
holds
ex
X0
being ( (
strict
boundary
) (
strict
TopSpace-like
proper
non
everywhere_dense
boundary
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( (
strict
boundary
) (
strict
TopSpace-like
proper
non
everywhere_dense
boundary
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) : ( ( ) ( )
set
) ;
theorem
:: TEX_3:52
for
X
being ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
)
for
A0
being ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) st
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) is
dense
holds
ex
X0
being ( (
strict
proper
dense
) (
strict
TopSpace-like
non
closed
proper
dense
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) st
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of )
=
the
carrier
of
X0
: ( (
strict
proper
dense
) (
strict
TopSpace-like
non
closed
proper
dense
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) : ( ( ) ( )
set
) ;
theorem
:: TEX_3:53
for
X
being ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
)
for
X1
being ( ( non
empty
boundary
) ( non
empty
TopSpace-like
non
open
proper
non
everywhere_dense
boundary
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) st
X1
: ( ( non
empty
boundary
) ( non
empty
TopSpace-like
non
open
proper
non
everywhere_dense
boundary
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) )
constitute_a_decomposition
;
theorem
:: TEX_3:54
for
X
being ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
)
for
X1
being ( ( non
empty
proper
dense
) ( non
empty
TopSpace-like
non
closed
proper
dense
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
boundary
) ( non
empty
strict
TopSpace-like
non
open
proper
non
everywhere_dense
boundary
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) st
X1
: ( ( non
empty
proper
dense
) ( non
empty
TopSpace-like
non
closed
proper
dense
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
boundary
) ( non
empty
strict
TopSpace-like
non
open
proper
non
everywhere_dense
boundary
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) )
constitute_a_decomposition
;
theorem
:: TEX_3:55
for
X
being ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
)
for
Y1
,
Y2
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
=
TopStruct
(# the
carrier
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) , the
topology
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) holds
(
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
boundary
) (
TopSpace-like
proper
non
everywhere_dense
boundary
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) iff
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
boundary
) (
TopSpace-like
proper
non
everywhere_dense
boundary
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopSpace
) ) ) ;
begin
theorem
:: TEX_3:56
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ( for
X0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds not
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
) holds
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
almost_discrete
;
theorem
:: TEX_3:57
for
X
being ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) st ( for
X0
being ( (
proper
) (
TopSpace-like
proper
)
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) holds not
X0
: ( (
proper
) (
TopSpace-like
proper
)
SubSpace
of
b
1
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
) holds
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) is
almost_discrete
;
registration
let
X
be ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopSpace
) ;
cluster
non
empty
->
non
empty
non
nowhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
proper
->
non
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
everywhere_dense
->
non
proper
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
non
empty
boundary
->
non
empty
non
closed
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
non
empty
closed
->
non
empty
non
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
proper
dense
->
non
open
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
open
dense
->
non
proper
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
cluster
open
proper
->
non
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
)
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
non
nowhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopStruct
) ) ;
end;
registration
let
X
be ( ( non
trivial
TopSpace-like
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopSpace
) ;
cluster
strict
TopSpace-like
non
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
trivial
TopSpace-like
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
almost_discrete
extremally_disconnected
hereditarily_extremally_disconnected
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:58
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ex
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
nowhere_dense
holds
not
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
almost_discrete
;
theorem
:: TEX_3:59
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ex
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
boundary
&
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
closed
) holds
not
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
almost_discrete
;
theorem
:: TEX_3:60
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ex
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
everywhere_dense
&
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
proper
) holds
not
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
almost_discrete
;
theorem
:: TEX_3:61
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st ex
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) st
(
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
dense
&
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
open
&
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
proper
) holds
not
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is
almost_discrete
;
registration
let
X
be ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
nowhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
strict
TopSpace-like
proper
everywhere_dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:62
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
nowhere_dense
holds
ex
X0
being ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TEX_3:63
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
A0
being ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) st
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) is
everywhere_dense
holds
ex
X0
being ( (
strict
proper
everywhere_dense
) (
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of )
=
the
carrier
of
X0
: ( (
strict
proper
everywhere_dense
) (
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( )
set
) ;
theorem
:: TEX_3:64
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X1
being ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
proper
everywhere_dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
X1
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
proper
everywhere_dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
constitute_a_decomposition
;
theorem
:: TEX_3:65
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X1
being ( ( non
empty
proper
everywhere_dense
) ( non
empty
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
X1
: ( ( non
empty
proper
everywhere_dense
) ( non
empty
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
constitute_a_decomposition
;
theorem
:: TEX_3:66
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
Y1
,
Y2
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) st
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
=
TopStruct
(# the
carrier
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) , the
topology
of
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) holds
(
Y1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
nowhere_dense
) (
TopSpace-like
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) iff
Y2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) is ( (
nowhere_dense
) (
TopSpace-like
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ) ;
registration
let
X
be ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ;
cluster
non
empty
strict
TopSpace-like
closed
boundary
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
strict
TopSpace-like
open
proper
dense
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopStruct
) ) ;
end;
theorem
:: TEX_3:67
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
A0
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
boundary
&
A0
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
closed
holds
ex
X0
being ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
A0
: ( ( non
empty
) ( non
empty
)
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TEX_3:68
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
A0
being ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) st
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) is
dense
&
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of ) is
open
holds
ex
X0
being ( (
strict
open
proper
dense
) (
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
A0
: ( ( non
empty
proper
) ( non
empty
proper
)
Subset
of )
=
the
carrier
of
X0
: ( (
strict
open
proper
dense
) (
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( )
set
) ;
theorem
:: TEX_3:69
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X1
being ( ( non
empty
closed
boundary
) ( non
empty
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
X1
: ( ( non
empty
closed
boundary
) ( non
empty
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
constitute_a_decomposition
;
theorem
:: TEX_3:70
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X1
being ( ( non
empty
open
proper
dense
) ( non
empty
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
X1
: ( ( non
empty
open
proper
dense
) ( non
empty
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
constitute_a_decomposition
;
theorem
:: TEX_3:71
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) holds
(
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is
nowhere_dense
iff ex
X1
being ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X1
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ) ) ;
theorem
:: TEX_3:72
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X0
being ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) holds
( (
X0
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is
boundary
&
X0
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is
closed
) or ex
X1
being ( ( non
empty
strict
proper
everywhere_dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
(
X1
: ( ( non
empty
strict
proper
everywhere_dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
meet
X2
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
=
TopStruct
(# the
carrier
of
X0
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
X0
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) &
X1
: ( ( non
empty
strict
proper
everywhere_dense
) ( non
empty
strict
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
union
X2
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
=
TopStruct
(# the
carrier
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) : ( ( ) ( non
empty
non
trivial
)
set
) , the
topology
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) : ( ( ) ( non
empty
non
trivial
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) ) ) ;
theorem
:: TEX_3:73
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X0
being ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) holds
( (
X0
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is
dense
&
X0
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is
open
) or ex
X1
being ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
(
X1
: ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
misses
X2
: ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) &
X1
: ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
union
X2
: ( ( non
empty
strict
nowhere_dense
) ( non
empty
strict
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( non
empty
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
=
TopStruct
(# the
carrier
of
X0
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
X0
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( non
empty
everywhere_dense
) ( non
empty
TopSpace-like
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
) ) ) ;
theorem
:: TEX_3:74
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X0
being ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X1
being ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
(
X1
: ( ( non
empty
strict
open
proper
dense
) ( non
empty
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ,
X2
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
constitute_a_decomposition
&
X0
: ( ( non
empty
nowhere_dense
) ( non
empty
TopSpace-like
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X2
: ( ( non
empty
strict
closed
boundary
) ( non
empty
strict
TopSpace-like
closed
non
open
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ) ) ;
theorem
:: TEX_3:75
for
X
being ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
)
for
X0
being ( (
proper
everywhere_dense
) (
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X1
being ( (
strict
open
proper
dense
) (
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ex
X2
being ( (
strict
closed
boundary
) (
strict
TopSpace-like
closed
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) st
(
X1
: ( (
strict
open
proper
dense
) (
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ,
X2
: ( (
strict
closed
boundary
) (
strict
TopSpace-like
closed
proper
non
dense
non
everywhere_dense
boundary
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) )
constitute_a_decomposition
&
X1
: ( (
strict
open
proper
dense
) (
strict
TopSpace-like
non
closed
open
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
proper
everywhere_dense
) (
TopSpace-like
non
closed
proper
dense
everywhere_dense
non
boundary
non
nowhere_dense
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
non
almost_discrete
) ( non
empty
non
trivial
TopSpace-like
non
discrete
non
anti-discrete
non
almost_discrete
)
TopSpace
) ) ) ) ;