:: Bases and Refinements of Topologies
:: by Grzegorz Bancerek
::
:: Received March 9, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users
begin
scheme
:: YELLOW_9:sch 1
FraenkelInvolution
{
F
1
()
->
non
empty
set
,
F
2
()
->
Subset
of
F
1
(),
F
3
()
->
Subset
of
F
1
(),
F
4
(
set
)
->
Element
of
F
1
() } :
F
2
()
=
{
F
4
(
a
) where
a
is
Element
of
F
1
() :
a
in
F
3
()
}
provided
A1
:
F
3
()
=
{
F
4
(
a
) where
a
is
Element
of
F
1
() :
a
in
F
2
()
}
and
A2
: for
a
being
Element
of
F
1
() holds
F
4
(
F
4
(
a
))
=
a
proof
end;
scheme
:: YELLOW_9:sch 2
FraenkelComplement1
{
F
1
()
->
non
empty
RelStr
,
F
2
()
->
Subset-Family
of
F
1
(),
F
3
()
->
set
,
F
4
(
set
)
->
Subset
of
F
1
() } :
COMPLEMENT
F
2
()
=
{
(
F
4
(
a
)
`
)
where
a
is
Element
of
F
1
() :
a
in
F
3
()
}
provided
A1
:
F
2
()
=
{
F
4
(
a
) where
a
is
Element
of
F
1
() :
a
in
F
3
()
}
proof
end;
scheme
:: YELLOW_9:sch 3
FraenkelComplement2
{
F
1
()
->
non
empty
RelStr
,
F
2
()
->
Subset-Family
of
F
1
(),
F
3
()
->
set
,
F
4
(
set
)
->
Subset
of
F
1
() } :
COMPLEMENT
F
2
()
=
{
F
4
(
a
) where
a
is
Element
of
F
1
() :
a
in
F
3
()
}
provided
A1
:
F
2
()
=
{
(
F
4
(
a
)
`
)
where
a
is
Element
of
F
1
() :
a
in
F
3
()
}
proof
end;
theorem
:: YELLOW_9:1
for
R
being non
empty
RelStr
for
x
,
y
being
Element
of
R
holds
(
y
in
(
uparrow
x
)
`
iff not
x
<=
y
)
proof
end;
scheme
:: YELLOW_9:sch 4
ABC
{
F
1
()
->
TopSpace
,
F
2
(
set
)
->
set
,
F
3
()
->
Function
,
P
1
[
set
] } :
F
3
()
"
(
union
{
F
2
(
x
) where
x
is
Subset
of
F
1
() :
P
1
[
x
]
}
)
=
union
{
(
F
3
()
"
F
2
(
y
)
)
where
y
is
Subset
of
F
1
() :
P
1
[
y
]
}
proof
end;
theorem
Th2
:
:: YELLOW_9:2
for
S
being
1-sorted
for
T
being non
empty
1-sorted
for
f
being
Function
of
S
,
T
for
X
being
Subset
of
T
holds
(
f
"
X
)
`
=
f
"
(
X
`
)
proof
end;
theorem
Th3
:
:: YELLOW_9:3
for
T
being
1-sorted
for
F
being
Subset-Family
of
T
holds
COMPLEMENT
F
=
{
(
a
`
)
where
a
is
Subset
of
T
:
a
in
F
}
proof
end;
theorem
Th4
:
:: YELLOW_9:4
for
R
being non
empty
RelStr
for
F
being
Subset
of
R
holds
(
uparrow
F
=
union
{
(
uparrow
x
)
where
x
is
Element
of
R
:
x
in
F
}
&
downarrow
F
=
union
{
(
downarrow
x
)
where
x
is
Element
of
R
:
x
in
F
}
)
proof
end;
theorem
:: YELLOW_9:5
for
R
being non
empty
RelStr
for
A
being
Subset-Family
of
R
for
F
being
Subset
of
R
st
A
=
{
(
(
uparrow
x
)
`
)
where
x
is
Element
of
R
:
x
in
F
}
holds
Intersect
A
=
(
uparrow
F
)
`
proof
end;
registration
cluster
non
empty
1
-element
correct
reflexive
transitive
antisymmetric
with_suprema
with_infima
complete
strict
for
TopRelStr
;
existence
ex
b
1
being
TopLattice
st
(
b
1
is
strict
&
b
1
is
complete
&
b
1
is 1
-element
)
proof
end;
end;
registration
let
S
be non
empty
RelStr
;
let
T
be non
empty
reflexive
antisymmetric
upper-bounded
RelStr
;
cluster
non
empty
Relation-like
the
carrier
of
S
-defined
the
carrier
of
T
-valued
Function-like
V27
( the
carrier
of
S
)
quasi_total
infs-preserving
for
Element
of
bool
[:
the
carrier
of
S
, the
carrier
of
T
:]
;
existence
ex
b
1
being
Function
of
S
,
T
st
b
1
is
infs-preserving
proof
end;
end;
registration
let
S
be non
empty
RelStr
;
let
T
be non
empty
reflexive
antisymmetric
lower-bounded
RelStr
;
cluster
non
empty
Relation-like
the
carrier
of
S
-defined
the
carrier
of
T
-valued
Function-like
V27
( the
carrier
of
S
)
quasi_total
sups-preserving
for
Element
of
bool
[:
the
carrier
of
S
, the
carrier
of
T
:]
;
existence
ex
b
1
being
Function
of
S
,
T
st
b
1
is
sups-preserving
proof
end;
end;
definition
let
R
,
S
be
1-sorted
;
assume
A1
: the
carrier
of
S
c=
the
carrier
of
R
;
A2
:
dom
(
id
the
carrier
of
S
)
=
the
carrier
of
S
;
A3
:
rng
(
id
the
carrier
of
S
)
=
the
carrier
of
S
;
func
incl
(
S
,
R
)
->
Function
of
S
,
R
equals
:
Def1
:
:: YELLOW_9:def 1
id
the
carrier
of
S
;
coherence
id
the
carrier
of
S
is
Function
of
S
,
R
by
A1
,
A2
,
A3
,
FUNCT_2:2
;
end;
::
deftheorem
Def1
defines
incl
YELLOW_9:def 1 :
for
R
,
S
being
1-sorted
st the
carrier
of
S
c=
the
carrier
of
R
holds
incl
(
S
,
R
)
=
id
the
carrier
of
S
;
registration
let
R
be non
empty
RelStr
;
let
S
be non
empty
SubRelStr
of
R
;
cluster
incl
(
S
,
R
)
->
monotone
;
coherence
incl
(
S
,
R
) is
monotone
proof
end;
end;
definition
let
R
be non
empty
RelStr
;
let
X
be non
empty
Subset
of
R
;
func
X
+id
->
non
empty
strict
NetStr
over
R
equals
:: YELLOW_9:def 2
(
incl
(
(
subrelstr
X
)
,
R
)
)
*
(
(
subrelstr
X
)
+id
)
;
coherence
(
incl
(
(
subrelstr
X
)
,
R
)
)
*
(
(
subrelstr
X
)
+id
)
is non
empty
strict
NetStr
over
R
;
func
X
opp+id
->
non
empty
strict
NetStr
over
R
equals
:: YELLOW_9:def 3
(
incl
(
(
subrelstr
X
)
,
R
)
)
*
(
(
subrelstr
X
)
opp+id
)
;
coherence
(
incl
(
(
subrelstr
X
)
,
R
)
)
*
(
(
subrelstr
X
)
opp+id
)
is non
empty
strict
NetStr
over
R
;
end;
::
deftheorem
defines
+id
YELLOW_9:def 2 :
for
R
being non
empty
RelStr
for
X
being non
empty
Subset
of
R
holds
X
+id
=
(
incl
(
(
subrelstr
X
)
,
R
)
)
*
(
(
subrelstr
X
)
+id
)
;
::
deftheorem
defines
opp+id
YELLOW_9:def 3 :
for
R
being non
empty
RelStr
for
X
being non
empty
Subset
of
R
holds
X
opp+id
=
(
incl
(
(
subrelstr
X
)
,
R
)
)
*
(
(
subrelstr
X
)
opp+id
)
;
theorem
:: YELLOW_9:6
for
R
being non
empty
RelStr
for
X
being non
empty
Subset
of
R
holds
( the
carrier
of
(
X
+id
)
=
X
&
X
+id
is
full
SubRelStr
of
R
& ( for
x
being
Element
of
(
X
+id
)
holds
(
X
+id
)
.
x
=
x
) )
proof
end;
theorem
:: YELLOW_9:7
for
R
being non
empty
RelStr
for
X
being non
empty
Subset
of
R
holds
( the
carrier
of
(
X
opp+id
)
=
X
&
X
opp+id
is
full
SubRelStr
of
R
opp
& ( for
x
being
Element
of
(
X
opp+id
)
holds
(
X
opp+id
)
.
x
=
x
) )
proof
end;
registration
let
R
be non
empty
reflexive
RelStr
;
let
X
be non
empty
Subset
of
R
;
cluster
X
+id
->
non
empty
reflexive
strict
;
coherence
X
+id
is
reflexive
;
cluster
X
opp+id
->
non
empty
reflexive
strict
;
coherence
X
opp+id
is
reflexive
;
end;
registration
let
R
be non
empty
transitive
RelStr
;
let
X
be non
empty
Subset
of
R
;
cluster
X
+id
->
non
empty
transitive
strict
;
coherence
X
+id
is
transitive
;
cluster
X
opp+id
->
non
empty
transitive
strict
;
coherence
X
opp+id
is
transitive
;
end;
registration
let
R
be non
empty
reflexive
RelStr
;
let
I
be
directed
Subset
of
R
;
cluster
subrelstr
I
->
directed
;
coherence
subrelstr
I
is
directed
proof
end;
end;
registration
let
R
be non
empty
reflexive
RelStr
;
let
I
be non
empty
directed
Subset
of
R
;
cluster
I
+id
->
non
empty
strict
directed
;
coherence
I
+id
is
directed
;
end;
registration
let
R
be non
empty
reflexive
RelStr
;
let
F
be non
empty
filtered
Subset
of
R
;
cluster
(
subrelstr
F
)
opp+id
->
directed
;
coherence
(
subrelstr
F
)
opp+id
is
directed
proof
end;
end;
registration
let
R
be non
empty
reflexive
RelStr
;
let
F
be non
empty
filtered
Subset
of
R
;
cluster
F
opp+id
->
non
empty
strict
directed
;
coherence
F
opp+id
is
directed
;
end;
begin
theorem
Th8
:
:: YELLOW_9:8
for
T
being
TopSpace
st
T
is
empty
holds
the
topology
of
T
=
{
{}
}
proof
end;
theorem
Th9
:
:: YELLOW_9:9
for
T
being 1
-element
TopSpace
holds
( the
topology
of
T
=
bool
the
carrier
of
T
& ( for
x
being
Point
of
T
holds
( the
carrier
of
T
=
{
x
}
& the
topology
of
T
=
{
{}
,
{
x
}
}
) ) )
proof
end;
theorem
:: YELLOW_9:10
for
T
being 1
-element
TopSpace
holds
(
{
the
carrier
of
T
}
is
Basis
of
T
&
{}
is
prebasis
of
T
&
{
{}
}
is
prebasis
of
T
)
proof
end;
theorem
Th11
:
:: YELLOW_9:11
for
X
,
Y
being
set
for
A
being
Subset-Family
of
X
st
A
=
{
Y
}
holds
(
FinMeetCl
A
=
{
Y
,
X
}
&
UniCl
A
=
{
Y
,
{}
}
)
proof
end;
theorem
:: YELLOW_9:12
for
X
being
set
for
A
,
B
being
Subset-Family
of
X
st (
A
=
B
\/
{
X
}
or
B
=
A
\
{
X
}
) holds
Intersect
A
=
Intersect
B
proof
end;
theorem
:: YELLOW_9:13
for
X
being
set
for
A
,
B
being
Subset-Family
of
X
st (
A
=
B
\/
{
X
}
or
B
=
A
\
{
X
}
) holds
FinMeetCl
A
=
FinMeetCl
B
proof
end;
theorem
Th14
:
:: YELLOW_9:14
for
X
being
set
for
A
being
Subset-Family
of
X
st
X
in
A
holds
for
x
being
set
holds
(
x
in
FinMeetCl
A
iff ex
Y
being non
empty
finite
Subset-Family
of
X
st
(
Y
c=
A
&
x
=
Intersect
Y
) )
proof
end;
theorem
Th15
:
:: YELLOW_9:15
for
X
being
set
for
A
being
Subset-Family
of
X
holds
UniCl
(
UniCl
A
)
=
UniCl
A
proof
end;
theorem
Th16
:
:: YELLOW_9:16
for
X
being
set
for
A
being
empty
Subset-Family
of
X
holds
UniCl
A
=
{
{}
}
proof
end;
theorem
Th17
:
:: YELLOW_9:17
for
X
being
set
for
A
being
empty
Subset-Family
of
X
holds
FinMeetCl
A
=
{
X
}
proof
end;
theorem
Th18
:
:: YELLOW_9:18
for
X
being
set
for
A
being
Subset-Family
of
X
st
A
=
{
{}
,
X
}
holds
(
UniCl
A
=
A
&
FinMeetCl
A
=
A
)
proof
end;
theorem
Th19
:
:: YELLOW_9:19
for
X
,
Y
being
set
for
A
being
Subset-Family
of
X
for
B
being
Subset-Family
of
Y
holds
( (
A
c=
B
implies
UniCl
A
c=
UniCl
B
) & (
A
=
B
implies
UniCl
A
=
UniCl
B
) )
proof
end;
theorem
Th20
:
:: YELLOW_9:20
for
X
,
Y
being
set
for
A
being
Subset-Family
of
X
for
B
being
Subset-Family
of
Y
st
A
=
B
&
X
in
A
holds
FinMeetCl
B
=
{
Y
}
\/
(
FinMeetCl
A
)
proof
end;
theorem
Th21
:
:: YELLOW_9:21
for
X
being
set
for
A
being
Subset-Family
of
X
holds
UniCl
(
FinMeetCl
(
UniCl
A
)
)
=
UniCl
(
FinMeetCl
A
)
proof
end;
begin
theorem
Th22
:
:: YELLOW_9:22
for
T
being
TopSpace
for
K
being
Subset-Family
of
T
holds
( the
topology
of
T
=
UniCl
K
iff
K
is
Basis
of
T
)
proof
end;
theorem
Th23
:
:: YELLOW_9:23
for
T
being
TopSpace
for
K
being
Subset-Family
of
T
holds
(
K
is
prebasis
of
T
iff
FinMeetCl
K
is
Basis
of
T
)
proof
end;
theorem
Th24
:
:: YELLOW_9:24
for
T
being non
empty
TopSpace
for
B
being
Subset-Family
of
T
st
UniCl
B
is
prebasis
of
T
holds
B
is
prebasis
of
T
proof
end;
theorem
Th25
:
:: YELLOW_9:25
for
T1
,
T2
being
TopSpace
for
B
being
Basis
of
T1
st the
carrier
of
T1
=
the
carrier
of
T2
&
B
is
Basis
of
T2
holds
the
topology
of
T1
=
the
topology
of
T2
proof
end;
theorem
Th26
:
:: YELLOW_9:26
for
T1
,
T2
being
TopSpace
for
P
being
prebasis
of
T1
st the
carrier
of
T1
=
the
carrier
of
T2
&
P
is
prebasis
of
T2
holds
the
topology
of
T1
=
the
topology
of
T2
proof
end;
theorem
:: YELLOW_9:27
for
T
being
TopSpace
for
K
being
Basis
of
T
holds
(
K
is
open
&
K
is
prebasis
of
T
) ;
theorem
:: YELLOW_9:28
for
T
being
TopSpace
for
K
being
prebasis
of
T
holds
K
is
open
;
theorem
Th29
:
:: YELLOW_9:29
for
T
being non
empty
TopSpace
for
B
being
prebasis
of
T
holds
B
\/
{
the
carrier
of
T
}
is
prebasis
of
T
proof
end;
theorem
:: YELLOW_9:30
for
T
being
TopSpace
for
B
being
Basis
of
T
holds
B
\/
{
the
carrier
of
T
}
is
Basis
of
T
proof
end;
theorem
Th31
:
:: YELLOW_9:31
for
T
being
TopSpace
for
B
being
Basis
of
T
for
A
being
Subset
of
T
holds
(
A
is
open
iff for
p
being
Point
of
T
st
p
in
A
holds
ex
a
being
Subset
of
T
st
(
a
in
B
&
p
in
a
&
a
c=
A
) )
proof
end;
theorem
Th32
:
:: YELLOW_9:32
for
T
being
TopSpace
for
B
being
Subset-Family
of
T
st
B
c=
the
topology
of
T
& ( for
A
being
Subset
of
T
st
A
is
open
holds
for
p
being
Point
of
T
st
p
in
A
holds
ex
a
being
Subset
of
T
st
(
a
in
B
&
p
in
a
&
a
c=
A
) ) holds
B
is
Basis
of
T
proof
end;
theorem
Th33
:
:: YELLOW_9:33
for
S
being
TopSpace
for
T
being non
empty
TopSpace
for
K
being
Basis
of
T
for
f
being
Function
of
S
,
T
holds
(
f
is
continuous
iff for
A
being
Subset
of
T
st
A
in
K
holds
f
"
(
A
`
)
is
closed
)
proof
end;
theorem
:: YELLOW_9:34
for
S
being
TopSpace
for
T
being non
empty
TopSpace
for
K
being
Basis
of
T
for
f
being
Function
of
S
,
T
holds
(
f
is
continuous
iff for
A
being
Subset
of
T
st
A
in
K
holds
f
"
A
is
open
)
proof
end;
theorem
Th35
:
:: YELLOW_9:35
for
S
being
TopSpace
for
T
being non
empty
TopSpace
for
K
being
prebasis
of
T
for
f
being
Function
of
S
,
T
holds
(
f
is
continuous
iff for
A
being
Subset
of
T
st
A
in
K
holds
f
"
(
A
`
)
is
closed
)
proof
end;
theorem
:: YELLOW_9:36
for
S
being
TopSpace
for
T
being non
empty
TopSpace
for
K
being
prebasis
of
T
for
f
being
Function
of
S
,
T
holds
(
f
is
continuous
iff for
A
being
Subset
of
T
st
A
in
K
holds
f
"
A
is
open
)
proof
end;
theorem
Th37
:
:: YELLOW_9:37
for
T
being non
empty
TopSpace
for
x
being
Point
of
T
for
X
being
Subset
of
T
for
K
being
Basis
of
T
st ( for
A
being
Subset
of
T
st
A
in
K
&
x
in
A
holds
A
meets
X
) holds
x
in
Cl
X
proof
end;
theorem
Th38
:
:: YELLOW_9:38
for
T
being non
empty
TopSpace
for
x
being
Point
of
T
for
X
being
Subset
of
T
for
K
being
prebasis
of
T
st ( for
Z
being
finite
Subset-Family
of
T
st
Z
c=
K
&
x
in
Intersect
Z
holds
Intersect
Z
meets
X
) holds
x
in
Cl
X
proof
end;
theorem
:: YELLOW_9:39
for
T
being non
empty
TopSpace
for
K
being
prebasis
of
T
for
x
being
Point
of
T
for
N
being
net
of
T
st ( for
A
being
Subset
of
T
st
A
in
K
&
x
in
A
holds
N
is_eventually_in
A
) holds
for
S
being
Subset
of
T
st
rng
(
netmap
(
N
,
T
)
)
c=
S
holds
x
in
Cl
S
proof
end;
begin
theorem
Th40
:
:: YELLOW_9:40
for
T1
,
T2
being non
empty
TopSpace
for
B1
being
Basis
of
T1
for
B2
being
Basis
of
T2
holds
{
[:
a
,
b
:]
where
a
is
Subset
of
T1
,
b
is
Subset
of
T2
: (
a
in
B1
&
b
in
B2
)
}
is
Basis
of
[:
T1
,
T2
:]
proof
end;
theorem
Th41
:
:: YELLOW_9:41
for
T1
,
T2
being non
empty
TopSpace
for
B1
being
prebasis
of
T1
for
B2
being
prebasis
of
T2
holds
{
[:
the
carrier
of
T1
,
b
:]
where
b
is
Subset
of
T2
:
b
in
B2
}
\/
{
[:
a
, the
carrier
of
T2
:]
where
a
is
Subset
of
T1
:
a
in
B1
}
is
prebasis
of
[:
T1
,
T2
:]
proof
end;
theorem
:: YELLOW_9:42
for
X1
,
X2
being
set
for
A
being
Subset-Family
of
[:
X1
,
X2
:]
for
A1
being non
empty
Subset-Family
of
X1
for
A2
being non
empty
Subset-Family
of
X2
st
A
=
{
[:
a
,
b
:]
where
a
is
Subset
of
X1
,
b
is
Subset
of
X2
: (
a
in
A1
&
b
in
A2
)
}
holds
Intersect
A
=
[:
(
Intersect
A1
)
,
(
Intersect
A2
)
:]
proof
end;
theorem
:: YELLOW_9:43
for
T1
,
T2
being non
empty
TopSpace
for
B1
being
prebasis
of
T1
for
B2
being
prebasis
of
T2
st
union
B1
=
the
carrier
of
T1
&
union
B2
=
the
carrier
of
T2
holds
{
[:
a
,
b
:]
where
a
is
Subset
of
T1
,
b
is
Subset
of
T2
: (
a
in
B1
&
b
in
B2
)
}
is
prebasis
of
[:
T1
,
T2
:]
proof
end;
begin
definition
let
R
be
RelStr
;
mode
TopAugmentation
of
R
->
TopRelStr
means
:
Def4
:
:: YELLOW_9:def 4
RelStr
(# the
carrier
of
it
, the
InternalRel
of
it
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#);
existence
ex
b
1
being
TopRelStr
st
RelStr
(# the
carrier
of
b
1
, the
InternalRel
of
b
1
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#)
proof
end;
end;
::
deftheorem
Def4
defines
TopAugmentation
YELLOW_9:def 4 :
for
R
being
RelStr
for
b
2
being
TopRelStr
holds
(
b
2
is
TopAugmentation
of
R
iff
RelStr
(# the
carrier
of
b
2
, the
InternalRel
of
b
2
#)
=
RelStr
(# the
carrier
of
R
, the
InternalRel
of
R
#) );
notation
let
R
be
RelStr
;
let
T
be
TopAugmentation
of
R
;
synonym
correct
T
for
TopSpace-like
;
end;
registration
let
R
be
RelStr
;
cluster
correct
discrete
strict
for
TopAugmentation
of
R
;
existence
ex
b
1
being
TopAugmentation
of
R
st
(
b
1
is
correct
&
b
1
is
discrete
&
b
1
is
strict
)
proof
end;
end;
theorem
:: YELLOW_9:44
for
T
being
TopRelStr
holds
T
is
TopAugmentation
of
T
proof
end;
theorem
:: YELLOW_9:45
for
S
being
TopRelStr
for
T
being
TopAugmentation
of
S
holds
S
is
TopAugmentation
of
T
proof
end;
theorem
:: YELLOW_9:46
for
R
being
RelStr
for
T1
being
TopAugmentation
of
R
for
T2
being
TopAugmentation
of
T1
holds
T2
is
TopAugmentation
of
R
proof
end;
registration
let
R
be non
empty
RelStr
;
cluster
->
non
empty
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
holds not
b
1
is
empty
proof
end;
end;
registration
let
R
be
reflexive
RelStr
;
cluster
->
reflexive
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
holds
b
1
is
reflexive
proof
end;
end;
registration
let
R
be
transitive
RelStr
;
cluster
->
transitive
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
holds
b
1
is
transitive
proof
end;
end;
registration
let
R
be
antisymmetric
RelStr
;
cluster
->
antisymmetric
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
holds
b
1
is
antisymmetric
proof
end;
end;
registration
let
R
be non
empty
complete
RelStr
;
cluster
->
complete
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
holds
b
1
is
complete
proof
end;
end;
theorem
Th47
:
:: YELLOW_9:47
for
S
being non
empty
reflexive
antisymmetric
up-complete
RelStr
for
T
being non
empty
reflexive
RelStr
st
RelStr
(# the
carrier
of
S
, the
InternalRel
of
S
#)
=
RelStr
(# the
carrier
of
T
, the
InternalRel
of
T
#) holds
for
A
being
Subset
of
S
for
C
being
Subset
of
T
st
A
=
C
&
A
is
inaccessible
holds
C
is
inaccessible
proof
end;
theorem
Th48
:
:: YELLOW_9:48
for
S
being non
empty
reflexive
RelStr
for
T
being
TopAugmentation
of
S
st the
topology
of
T
=
sigma
S
holds
T
is
correct
proof
end;
theorem
Th49
:
:: YELLOW_9:49
for
S
being
complete
LATTICE
for
T
being
TopAugmentation
of
S
st the
topology
of
T
=
sigma
S
holds
T
is
Scott
proof
end;
registration
let
R
be
complete
LATTICE
;
cluster
non
empty
correct
reflexive
transitive
antisymmetric
with_suprema
with_infima
complete
lower-bounded
upper-bounded
V194
()
up-complete
/\-complete
strict
Scott
for
TopAugmentation
of
R
;
existence
ex
b
1
being
TopAugmentation
of
R
st
(
b
1
is
Scott
&
b
1
is
strict
&
b
1
is
correct
)
proof
end;
end;
theorem
Th50
:
:: YELLOW_9:50
for
S
,
T
being non
empty
reflexive
transitive
antisymmetric
complete
Scott
TopRelStr
st
RelStr
(# the
carrier
of
S
, the
InternalRel
of
S
#)
=
RelStr
(# the
carrier
of
T
, the
InternalRel
of
T
#) holds
for
F
being
Subset
of
S
for
G
being
Subset
of
T
st
F
=
G
&
F
is
open
holds
G
is
open
proof
end;
theorem
Th51
:
:: YELLOW_9:51
for
S
being
complete
LATTICE
for
T
being
Scott
TopAugmentation
of
S
holds the
topology
of
T
=
sigma
S
proof
end;
theorem
:: YELLOW_9:52
for
S
,
T
being
complete
LATTICE
st
RelStr
(# the
carrier
of
S
, the
InternalRel
of
S
#)
=
RelStr
(# the
carrier
of
T
, the
InternalRel
of
T
#) holds
sigma
S
=
sigma
T
proof
end;
registration
let
R
be
complete
LATTICE
;
cluster
Scott
->
correct
for
TopAugmentation
of
R
;
coherence
for
b
1
being
TopAugmentation
of
R
st
b
1
is
Scott
holds
b
1
is
correct
proof
end;
end;
Lm1
:
for
S
being
TopStruct
ex
T
being
strict
TopSpace
st
( the
carrier
of
T
=
the
carrier
of
S
& the
topology
of
S
is
prebasis
of
T
)
proof
end;
begin
definition
let
T
be
TopStruct
;
mode
TopExtension
of
T
->
TopSpace
means
:
Def5
:
:: YELLOW_9:def 5
( the
carrier
of
T
=
the
carrier
of
it
& the
topology
of
T
c=
the
topology
of
it
);
existence
ex
b
1
being
TopSpace
st
( the
carrier
of
T
=
the
carrier
of
b
1
& the
topology
of
T
c=
the
topology
of
b
1
)
proof
end;
end;
::
deftheorem
Def5
defines
TopExtension
YELLOW_9:def 5 :
for
T
being
TopStruct
for
b
2
being
TopSpace
holds
(
b
2
is
TopExtension
of
T
iff ( the
carrier
of
T
=
the
carrier
of
b
2
& the
topology
of
T
c=
the
topology
of
b
2
) );
theorem
Th53
:
:: YELLOW_9:53
for
S
being
TopStruct
ex
T
being
TopExtension
of
S
st
(
T
is
strict
& the
topology
of
S
is
prebasis
of
T
)
proof
end;
registration
let
T
be
TopStruct
;
cluster
strict
correct
discrete
for
TopExtension
of
T
;
existence
ex
b
1
being
TopExtension
of
T
st
(
b
1
is
strict
&
b
1
is
discrete
)
proof
end;
end;
definition
let
T1
,
T2
be
TopStruct
;
mode
Refinement
of
T1
,
T2
->
TopSpace
means
:
Def6
:
:: YELLOW_9:def 6
( the
carrier
of
it
=
the
carrier
of
T1
\/
the
carrier
of
T2
& the
topology
of
T1
\/
the
topology
of
T2
is
prebasis
of
it
);
existence
ex
b
1
being
TopSpace
st
( the
carrier
of
b
1
=
the
carrier
of
T1
\/
the
carrier
of
T2
& the
topology
of
T1
\/
the
topology
of
T2
is
prebasis
of
b
1
)
proof
end;
end;
::
deftheorem
Def6
defines
Refinement
YELLOW_9:def 6 :
for
T1
,
T2
being
TopStruct
for
b
3
being
TopSpace
holds
(
b
3
is
Refinement
of
T1
,
T2
iff ( the
carrier
of
b
3
=
the
carrier
of
T1
\/
the
carrier
of
T2
& the
topology
of
T1
\/
the
topology
of
T2
is
prebasis
of
b
3
) );
registration
let
T1
be non
empty
TopStruct
;
let
T2
be
TopStruct
;
cluster
->
non
empty
for
Refinement
of
T1
,
T2
;
coherence
for
b
1
being
Refinement
of
T1
,
T2
holds not
b
1
is
empty
proof
end;
cluster
->
non
empty
for
Refinement
of
T2
,
T1
;
coherence
for
b
1
being
Refinement
of
T2
,
T1
holds not
b
1
is
empty
proof
end;
end;
theorem
:: YELLOW_9:54
for
T1
,
T2
being
TopStruct
for
T
,
T9
being
Refinement
of
T1
,
T2
holds
TopStruct
(# the
carrier
of
T
, the
topology
of
T
#)
=
TopStruct
(# the
carrier
of
T9
, the
topology
of
T9
#)
proof
end;
theorem
:: YELLOW_9:55
for
T1
,
T2
being
TopStruct
for
T
being
Refinement
of
T1
,
T2
holds
T
is
Refinement
of
T2
,
T1
proof
end;
theorem
:: YELLOW_9:56
for
T1
,
T2
being
TopStruct
for
T
being
Refinement
of
T1
,
T2
for
X
being
Subset-Family
of
T
st
X
=
the
topology
of
T1
\/
the
topology
of
T2
holds
the
topology
of
T
=
UniCl
(
FinMeetCl
X
)
proof
end;
theorem
:: YELLOW_9:57
for
T1
,
T2
being
TopStruct
st the
carrier
of
T1
=
the
carrier
of
T2
holds
for
T
being
Refinement
of
T1
,
T2
holds
(
T
is
TopExtension
of
T1
&
T
is
TopExtension
of
T2
)
proof
end;
theorem
:: YELLOW_9:58
for
T1
,
T2
being non
empty
TopSpace
for
T
being
Refinement
of
T1
,
T2
for
B1
being
prebasis
of
T1
for
B2
being
prebasis
of
T2
holds
(
B1
\/
B2
)
\/
{
the
carrier
of
T1
, the
carrier
of
T2
}
is
prebasis
of
T
proof
end;
theorem
Th59
:
:: YELLOW_9:59
for
T1
,
T2
being non
empty
TopSpace
for
B1
being
Basis
of
T1
for
B2
being
Basis
of
T2
for
T
being
Refinement
of
T1
,
T2
holds
(
B1
\/
B2
)
\/
(
INTERSECTION
(
B1
,
B2
)
)
is
Basis
of
T
proof
end;
theorem
Th60
:
:: YELLOW_9:60
for
T1
,
T2
being non
empty
TopSpace
st the
carrier
of
T1
=
the
carrier
of
T2
holds
for
T
being
Refinement
of
T1
,
T2
holds
INTERSECTION
( the
topology
of
T1
, the
topology
of
T2
) is
Basis
of
T
proof
end;
theorem
:: YELLOW_9:61
for
L
being non
empty
RelStr
for
T1
,
T2
being
correct
TopAugmentation
of
L
for
T
being
Refinement
of
T1
,
T2
holds
INTERSECTION
( the
topology
of
T1
, the
topology
of
T2
) is
Basis
of
T
proof
end;