:: TOPS_3 semantic presentation
begin
theorem
:: TOPS_3:1
for
X
being ( ( ) ( )
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) holds
( (
A
: ( ( ) ( )
Subset
of )
=
{}
X
: ( ( ) ( )
TopStruct
) : ( ( ) (
empty
boundary
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) implies
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
[#]
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( non
proper
dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) & (
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
[#]
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( non
proper
dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) implies
A
: ( ( ) ( )
Subset
of )
=
{}
X
: ( ( ) ( )
TopStruct
) : ( ( ) (
empty
boundary
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) & (
A
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) ( )
set
) implies
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) & (
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) implies
A
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) ( )
set
) ) ) ;
theorem
:: TOPS_3:2
for
X
being ( ( ) ( )
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) holds
( (
A
: ( ( ) ( )
Subset
of )
=
[#]
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( non
proper
dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) implies
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
X
: ( ( ) ( )
TopStruct
) : ( ( ) (
empty
boundary
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) & (
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
X
: ( ( ) ( )
TopStruct
) : ( ( ) (
empty
boundary
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) implies
A
: ( ( ) ( )
Subset
of )
=
[#]
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( non
proper
dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) & (
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) implies
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
set
) ) & (
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
set
) implies
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) ) ;
theorem
:: TOPS_3:3
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
/\
(
Cl
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
Cl
(
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:4
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
Int
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
\/
(
Int
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:5
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
B
,
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
closed
holds
Int
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
Subset
of )
\/
(
Int
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:6
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
B
,
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
closed
holds
Int
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
Int
(
A
: ( ( ) ( )
Subset
of )
\/
(
Int
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:7
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
misses
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) holds
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPS_3:8
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
\/
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) holds
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ;
begin
definition
let
X
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
boundary
means
:: TOPS_3:def 1
Int
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
set
) ;
end;
theorem
:: TOPS_3:9
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
{}
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
open
closed
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) is
boundary
;
theorem
:: TOPS_3:10
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
boundary
holds
A
: ( ( ) ( )
Subset
of )
<>
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TOPS_3:11
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
B
,
A
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of ) is
boundary
&
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TOPS_3:12
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
boundary
iff for
C
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
C
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of ) is
closed
holds
C
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:13
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
boundary
iff for
G
being ( ( ) ( )
Subset
of ) st
G
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) ( )
set
) &
G
: ( ( ) ( )
Subset
of ) is
open
holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
meets
G
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: TOPS_3:14
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
boundary
iff for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset
of ) is
closed
holds
Int
F
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
Int
(
F
: ( ( ) ( )
Subset
of )
\/
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: TOPS_3:15
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
boundary
holds
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) is
boundary
;
definition
let
X
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
dense
means
:: TOPS_3:def 2
Cl
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ;
end;
theorem
:: TOPS_3:16
for
X
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
[#]
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
proper
open
closed
dense
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) is
dense
;
theorem
:: TOPS_3:17
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
dense
holds
A
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPS_3:18
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
dense
iff
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
boundary
) ;
theorem
:: TOPS_3:19
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
dense
iff for
C
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of ) is
closed
holds
C
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPS_3:20
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
dense
iff for
G
being ( ( ) ( )
Subset
of ) st
G
: ( ( ) ( )
Subset
of ) is
open
holds
Cl
G
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
Cl
(
G
: ( ( ) ( )
Subset
of )
/\
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: TOPS_3:21
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
dense
holds
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
dense
;
definition
let
X
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
nowhere_dense
means
:: TOPS_3:def 3
Int
(
Cl
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
set
) ;
end;
theorem
:: TOPS_3:22
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
{}
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
open
closed
boundary
nowhere_dense
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
nowhere_dense
;
theorem
:: TOPS_3:23
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
A
: ( ( ) ( )
Subset
of )
<>
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: TOPS_3:24
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
nowhere_dense
;
theorem
:: TOPS_3:25
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
not
A
: ( ( ) ( )
Subset
of ) is
dense
;
theorem
:: TOPS_3:26
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
B
,
A
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
&
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
;
theorem
:: TOPS_3:27
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
iff ex
C
being ( ( ) ( )
Subset
of ) st
(
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of ) is
closed
&
C
: ( ( ) ( )
Subset
of ) is
boundary
) ) ;
theorem
:: TOPS_3:28
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
iff for
G
being ( ( ) ( )
Subset
of ) st
G
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) ( )
set
) &
G
: ( ( ) ( )
Subset
of ) is
open
holds
ex
H
being ( ( ) ( )
Subset
of ) st
(
H
: ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) &
H
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) ( )
set
) &
H
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
misses
H
: ( ( ) ( )
Subset
of ) ) ) ;
theorem
:: TOPS_3:29
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
nowhere_dense
;
theorem
:: TOPS_3:30
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
&
B
: ( ( ) ( )
Subset
of ) is
boundary
holds
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
boundary
;
definition
let
X
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
everywhere_dense
means
:: TOPS_3:def 4
Cl
(
Int
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
[#]
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( non
proper
dense
)
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
X
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
everywhere_dense
means
:: TOPS_3:def 5
Cl
(
Int
A
: ( ( ) ( )
Element
of
K10
(
K10
(
X
: ( ( ) ( )
TopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ;
end;
theorem
:: TOPS_3:31
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) holds
[#]
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
non
proper
open
closed
dense
non
boundary
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
everywhere_dense
;
theorem
:: TOPS_3:32
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
everywhere_dense
;
theorem
:: TOPS_3:33
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
A
: ( ( ) ( )
Subset
of ) is
dense
;
theorem
:: TOPS_3:34
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
A
: ( ( ) ( )
Subset
of )
<>
{}
: ( ( ) ( )
set
) ;
theorem
:: TOPS_3:35
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
iff
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
dense
) ;
theorem
:: TOPS_3:36
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of ) is
dense
holds
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
;
theorem
:: TOPS_3:37
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
not
A
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TOPS_3:38
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
;
theorem
:: TOPS_3:39
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
iff
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
nowhere_dense
) ;
theorem
:: TOPS_3:40
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
iff
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
everywhere_dense
) ;
theorem
:: TOPS_3:41
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
iff ex
C
being ( ( ) ( )
Subset
of ) st
(
C
: ( ( ) ( )
Subset
of )
c=
A
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of ) is
dense
) ) ;
theorem
:: TOPS_3:42
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
iff for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset
of )
<>
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) &
F
: ( ( ) ( )
Subset
of ) is
closed
holds
ex
H
being ( ( ) ( )
Subset
of ) st
(
F
: ( ( ) ( )
Subset
of )
c=
H
: ( ( ) ( )
Subset
of ) &
H
: ( ( ) ( )
Subset
of )
<>
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) &
H
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
\/
H
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPS_3:43
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
everywhere_dense
;
theorem
:: TOPS_3:44
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
everywhere_dense
;
theorem
:: TOPS_3:45
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
B
: ( ( ) ( )
Subset
of ) is
dense
holds
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
dense
;
theorem
:: TOPS_3:46
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
dense
&
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
A
: ( ( ) ( )
Subset
of )
\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
dense
;
theorem
:: TOPS_3:47
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
B
: ( ( ) ( )
Subset
of ) is
boundary
holds
A
: ( ( ) ( )
Subset
of )
\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
dense
;
theorem
:: TOPS_3:48
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
A
: ( ( ) ( )
Subset
of )
\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
everywhere_dense
;
theorem
:: TOPS_3:49
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
D
being ( ( ) ( )
Subset
of ) st
D
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
ex
C
,
B
being ( ( ) ( )
Subset
of ) st
(
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of ) is
dense
&
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
&
C
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
D
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of )
misses
B
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: TOPS_3:50
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
D
being ( ( ) ( )
Subset
of ) st
D
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
ex
C
,
B
being ( ( ) ( )
Subset
of ) st
(
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of ) is
dense
&
B
: ( ( ) ( )
Subset
of ) is
closed
&
B
: ( ( ) ( )
Subset
of ) is
boundary
&
C
: ( ( ) ( )
Subset
of )
\/
(
D
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
D
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of )
misses
B
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPS_3:51
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
D
being ( ( ) ( )
Subset
of ) st
D
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
ex
C
,
B
being ( ( ) ( )
Subset
of ) st
(
C
: ( ( ) ( )
Subset
of ) is
closed
&
C
: ( ( ) ( )
Subset
of ) is
boundary
&
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
C
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
D
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPS_3:52
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
D
being ( ( ) ( )
Subset
of ) st
D
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
ex
C
,
B
being ( ( ) ( )
Subset
of ) st
(
C
: ( ( ) ( )
Subset
of ) is
closed
&
C
: ( ( ) ( )
Subset
of ) is
boundary
&
B
: ( ( ) ( )
Subset
of ) is
open
&
B
: ( ( ) ( )
Subset
of ) is
dense
&
C
: ( ( ) ( )
Subset
of )
/\
(
D
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
D
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of )
misses
B
: ( ( ) ( )
Subset
of ) &
C
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ;
begin
theorem
:: TOPS_3:53
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
c=
A
: ( ( ) ( )
Subset
of ) holds
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:54
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( ( ) (
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of ) is
closed
&
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
Y0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:55
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( ( non
empty
closed
) ( non
empty
TopSpace-like
closed
)
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
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
2
: ( ( non
empty
closed
) ( non
empty
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:56
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( ( ) (
TopSpace-like
)
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 )
c=
B
: ( ( ) ( )
Subset
of ) holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
Int
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
2
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:57
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
Int
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:58
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
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
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
Int
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
2
: ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:59
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 )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
dense
holds
B
: ( ( ) ( )
Subset
of ) is
dense
;
theorem
:: TOPS_3:60
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
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( ) (
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
( (
C
: ( ( ) ( )
Subset
of ) is
dense
&
B
: ( ( ) ( )
Subset
of ) is
dense
) iff
A
: ( ( ) ( )
Subset
of ) is
dense
) ;
theorem
:: TOPS_3:61
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
) )
for
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
;
theorem
:: TOPS_3:62
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
) )
for
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
( (
C
: ( ( ) ( )
Subset
of ) is
dense
&
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) iff
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) ;
theorem
:: TOPS_3:63
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
,
C
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of )
=
the
carrier
of
X0
: ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
( (
C
: ( ( ) ( )
Subset
of ) is
dense
&
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) iff
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) ;
theorem
:: TOPS_3:64
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
) )
for
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) holds
( (
C
: ( ( ) ( )
Subset
of ) is
everywhere_dense
&
B
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) iff
A
: ( ( ) ( )
Subset
of ) is
everywhere_dense
) ;
theorem
:: TOPS_3:65
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
) )
for
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of ) is
boundary
holds
A
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TOPS_3:66
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
) )
for
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
boundary
holds
B
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TOPS_3:67
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
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
(
A
: ( ( ) ( )
Subset
of ) is
boundary
iff
B
: ( ( ) ( )
Subset
of ) is
boundary
) ;
theorem
:: TOPS_3:68
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
) )
for
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
;
theorem
:: TOPS_3:69
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
) )
for
C
,
A
being ( ( ) ( )
Subset
of )
for
B
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of ) is
open
&
C
: ( ( ) ( )
Subset
of )
c=
the
carrier
of
X0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) : ( ( ) ( non
empty
)
set
) &
A
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
;
theorem
:: TOPS_3:70
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
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
(
A
: ( ( ) ( )
Subset
of ) is
nowhere_dense
iff
B
: ( ( ) ( )
Subset
of ) is
nowhere_dense
) ;
begin
theorem
:: TOPS_3:71
for
X1
,
X2
being ( ( ) ( )
1-sorted
) st the
carrier
of
X1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
=
the
carrier
of
X2
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) holds
for
C1
being ( ( ) ( )
Subset
of )
for
C2
being ( ( ) ( )
Subset
of ) holds
(
C1
: ( ( ) ( )
Subset
of )
=
C2
: ( ( ) ( )
Subset
of ) iff
C1
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
C2
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K10
( the
carrier
of
b
2
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: TOPS_3:72
for
X1
,
X2
being ( ( ) ( )
TopStruct
) st the
carrier
of
X1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
=
the
carrier
of
X2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) & ( for
C1
being ( ( ) ( )
Subset
of )
for
C2
being ( ( ) ( )
Subset
of ) st
C1
: ( ( ) ( )
Subset
of )
=
C2
: ( ( ) ( )
Subset
of ) holds
(
C1
: ( ( ) ( )
Subset
of ) is
open
iff
C2
: ( ( ) ( )
Subset
of ) is
open
) ) holds
TopStruct
(# the
carrier
of
X1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
) ;
theorem
:: TOPS_3:73
for
X1
,
X2
being ( ( ) ( )
TopStruct
) st the
carrier
of
X1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
=
the
carrier
of
X2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) & ( for
C1
being ( ( ) ( )
Subset
of )
for
C2
being ( ( ) ( )
Subset
of ) st
C1
: ( ( ) ( )
Subset
of )
=
C2
: ( ( ) ( )
Subset
of ) holds
(
C1
: ( ( ) ( )
Subset
of ) is
closed
iff
C2
: ( ( ) ( )
Subset
of ) is
closed
) ) holds
TopStruct
(# the
carrier
of
X1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
) ;
theorem
:: TOPS_3:74
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
=
the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) & ( for
C1
being ( ( ) ( )
Subset
of )
for
C2
being ( ( ) ( )
Subset
of ) st
C1
: ( ( ) ( )
Subset
of )
=
C2
: ( ( ) ( )
Subset
of ) holds
Int
C1
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
Int
C2
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) holds
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) ;
theorem
:: TOPS_3:75
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) st the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
=
the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) & ( for
C1
being ( ( ) ( )
Subset
of )
for
C2
being ( ( ) ( )
Subset
of ) st
C1
: ( ( ) ( )
Subset
of )
=
C2
: ( ( ) ( )
Subset
of ) holds
Cl
C1
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
Cl
C2
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) holds
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) ;
theorem
:: TOPS_3:76
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) &
D1
: ( ( ) ( )
Subset
of ) is
open
holds
D2
: ( ( ) ( )
Subset
of ) is
open
;
theorem
:: TOPS_3:77
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) holds
Int
D1
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
Int
D2
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:78
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
c=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) holds
Int
D1
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
Int
D2
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:79
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) &
D1
: ( ( ) ( )
Subset
of ) is
closed
holds
D2
: ( ( ) ( )
Subset
of ) is
closed
;
theorem
:: TOPS_3:80
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) holds
Cl
D1
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
Cl
D2
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:81
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
c=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) holds
Cl
D1
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
Cl
D2
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: TOPS_3:82
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D2
: ( ( ) ( )
Subset
of )
c=
D1
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) &
D1
: ( ( ) ( )
Subset
of ) is
boundary
holds
D2
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TOPS_3:83
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
c=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) &
D1
: ( ( ) ( )
Subset
of ) is
dense
holds
D2
: ( ( ) ( )
Subset
of ) is
dense
;
theorem
:: TOPS_3:84
for
X1
,
X2
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D2
: ( ( ) ( )
Subset
of )
c=
D1
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
topology
of
X2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
2
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
TopSpace-like
)
TopStruct
) &
D1
: ( ( ) ( )
Subset
of ) is
nowhere_dense
holds
D2
: ( ( ) ( )
Subset
of ) is
nowhere_dense
;
theorem
:: TOPS_3:85
for
X1
,
X2
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
D1
being ( ( ) ( )
Subset
of )
for
D2
being ( ( ) ( )
Subset
of ) st
D1
: ( ( ) ( )
Subset
of )
c=
D2
: ( ( ) ( )
Subset
of ) &
TopStruct
(# the
carrier
of
X1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) , the
topology
of
X1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
Element
of
K10
(
K10
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
TopStruct
)
=
TopStruct
(# the
carrier
of
X2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) , the
topology
of
X2
: ( ( 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
) &
D1
: ( ( ) ( )
Subset
of ) is
everywhere_dense
holds
D2
: ( ( ) ( )
Subset
of ) is
everywhere_dense
;