:: TEX_4 semantic presentation
begin
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
cluster
Cl
A
: ( ( non
empty
) ( non
empty
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
non
empty
;
end;
registration
let
X
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
empty
) (
empty
trivial
open
closed
boundary
nowhere_dense
)
Subset
of ) ;
cluster
Cl
A
: ( (
empty
) (
empty
trivial
open
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
X
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
->
empty
;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( non
proper
) ( non
empty
non
proper
)
Subset
of ) ;
cluster
Cl
A
: ( ( non
proper
) ( non
empty
non
proper
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
non
proper
;
end;
registration
let
X
be ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( non
trivial
) ( non
empty
non
trivial
)
Subset
of ) ;
cluster
Cl
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
Element
of
bool
the
carrier
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
trivial
TopSpace-like
) ( non
empty
non
trivial
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
->
non
trivial
;
end;
theorem
:: TEX_4:1
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
meet
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:2
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
meet
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( non
proper
) ( non
empty
non
proper
)
Subset
of ) ;
cluster
Int
A
: ( ( non
proper
) ( non
empty
non
proper
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
non
proper
;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
proper
) (
proper
)
Subset
of ) ;
cluster
Int
A
: ( (
proper
) (
proper
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
proper
;
end;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
empty
) (
empty
trivial
proper
open
closed
boundary
nowhere_dense
)
Subset
of ) ;
cluster
Int
A
: ( (
empty
) (
empty
trivial
proper
open
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
empty
trivial
proper
open
closed
boundary
nowhere_dense
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
empty
;
end;
theorem
:: TEX_4:3
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
union
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
G
: ( ( ) ( )
Subset
of )
c=
A
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
begin
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
IT
be ( ( ) ( )
Subset
of ) ;
attr
IT
is
anti-discrete
means
:: TEX_4:def 1
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
G
being ( ( ) ( )
Subset
of ) st
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
G
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
Point
of ( ( ) ( )
set
) )
in
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
c=
G
: ( ( ) ( )
Subset
of ) ;
end;
definition
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
anti-discrete
means
:: TEX_4:def 2
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
F
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( ) ( )
Subset
of ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
c=
F
: ( ( ) ( )
Subset
of ) ;
end;
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
anti-discrete
means
:: TEX_4:def 3
for
G
being ( ( ) ( )
Subset
of ) holds
( not
G
: ( ( ) ( )
Subset
of ) is
open
or
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
misses
G
: ( ( ) ( )
Subset
of ) or
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
c=
G
: ( ( ) ( )
Subset
of ) );
end;
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
anti-discrete
means
:: TEX_4:def 4
for
F
being ( ( ) ( )
Subset
of ) holds
( not
F
: ( ( ) ( )
Subset
of ) is
closed
or
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
misses
F
: ( ( ) ( )
Subset
of ) or
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
c=
F
: ( ( ) ( )
Subset
of ) );
end;
theorem
:: TEX_4:4
for
Y0
,
Y1
being ( ( ) ( )
TopStruct
)
for
D0
being ( ( ) ( )
Subset
of )
for
D1
being ( ( ) ( )
Subset
of ) st
TopStruct
(# the
carrier
of
Y0
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
Y0
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
Y1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
Y1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
) &
D0
: ( ( ) ( )
Subset
of )
=
D1
: ( ( ) ( )
Subset
of ) &
D0
: ( ( ) ( )
Subset
of ) is
anti-discrete
holds
D1
: ( ( ) ( )
Subset
of ) is
anti-discrete
;
theorem
:: TEX_4:5
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
c=
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
holds
B
: ( ( ) ( )
Subset
of ) is
anti-discrete
;
theorem
:: TEX_4:6
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
anti-discrete
;
theorem
:: TEX_4:7
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( (
empty
) (
empty
trivial
proper
boundary
)
Subset
of ) holds
A
: ( (
empty
) (
empty
trivial
proper
boundary
)
Subset
of ) is
anti-discrete
;
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
IT
be ( ( ) ( )
Subset-Family
of ) ;
attr
IT
is
anti-discrete-set-family
means
:: TEX_4:def 5
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
in
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
;
end;
theorem
:: TEX_4:8
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of ) is
anti-discrete-set-family
&
meet
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
<>
{}
: ( ( ) (
empty
trivial
)
set
) holds
union
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
anti-discrete
;
theorem
:: TEX_4:9
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
F
being ( ( ) ( )
Subset-Family
of ) st
F
: ( ( ) ( )
Subset-Family
of ) is
anti-discrete-set-family
holds
meet
F
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
anti-discrete
;
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ;
func
MaxADSF
x
->
( ( ) ( )
Subset-Family
of )
equals
:: TEX_4:def 6
{
A
: ( ( ) ( )
Subset
of ) where
A
is ( ( ) ( )
Subset
of ) : (
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
&
x
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
in
A
: ( ( ) ( )
Subset
of ) )
}
;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
MaxADSF
x
: ( ( ) ( )
Element
of the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset-Family
of )
->
non
empty
;
end;
theorem
:: TEX_4:10
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSF
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset-Family
of ) is
anti-discrete-set-family
;
theorem
:: TEX_4:11
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
meet
(
MaxADSF
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:12
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
union
(
MaxADSF
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:13
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
union
(
MaxADSF
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
)
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
anti-discrete
;
begin
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
IT
be ( ( ) ( )
Subset
of ) ;
attr
IT
is
maximal_anti-discrete
means
:: TEX_4:def 7
(
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) is
anti-discrete
& ( for
D
being ( ( ) ( )
Subset
of ) st
D
: ( ( ) ( )
Subset
of ) is
anti-discrete
&
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
c=
D
: ( ( ) ( )
Subset
of ) holds
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
=
D
: ( ( ) ( )
Subset
of ) ) );
end;
theorem
:: TEX_4:14
for
Y0
,
Y1
being ( ( ) ( )
TopStruct
)
for
D0
being ( ( ) ( )
Subset
of )
for
D1
being ( ( ) ( )
Subset
of ) st
TopStruct
(# the
carrier
of
Y0
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
Y0
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
Y1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
topology
of
Y1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
b
2
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
TopStruct
) &
D0
: ( ( ) ( )
Subset
of )
=
D1
: ( ( ) ( )
Subset
of ) &
D0
: ( ( ) ( )
Subset
of ) is
maximal_anti-discrete
holds
D1
: ( ( ) ( )
Subset
of ) is
maximal_anti-discrete
;
theorem
:: TEX_4:15
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( (
empty
) (
empty
trivial
proper
boundary
)
Subset
of ) holds not
A
: ( (
empty
) (
empty
trivial
proper
boundary
)
Subset
of ) is
maximal_anti-discrete
;
theorem
:: TEX_4:16
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
anti-discrete
&
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
open
holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
maximal_anti-discrete
;
theorem
:: TEX_4:17
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
anti-discrete
&
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
closed
holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is
maximal_anti-discrete
;
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ;
func
MaxADSet
x
->
( ( ) ( )
Subset
of )
equals
:: TEX_4:def 8
union
(
MaxADSF
x
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Subset-Family
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
MaxADSet
x
: ( ( ) ( )
Element
of the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
->
non
empty
;
end;
theorem
:: TEX_4:18
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) ;
theorem
:: TEX_4:19
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
D
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
D
: ( ( ) ( )
Subset
of ) is
anti-discrete
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
D
: ( ( ) ( )
Subset
of ) holds
D
: ( ( ) ( )
Subset
of )
c=
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) ;
theorem
:: TEX_4:20
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) is
maximal_anti-discrete
;
theorem
:: TEX_4:21
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) iff
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
=
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) ) ;
theorem
:: TEX_4:22
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
misses
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) or
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
=
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) ) ;
theorem
:: TEX_4:23
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
F
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
F
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( ) ( )
Subset
of ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:24
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
G
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
G
: ( ( ) ( )
Subset
of ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:25
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
meet
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:26
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
definition
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
maximal_anti-discrete
means
:: TEX_4:def 9
ex
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) &
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
=
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) );
end;
theorem
:: TEX_4:27
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of ) is
maximal_anti-discrete
holds
A
: ( ( ) ( )
Subset
of )
=
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) ;
definition
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
redefine
attr
A
is
maximal_anti-discrete
means
:: TEX_4:def 10
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
=
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
end;
definition
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
func
MaxADSet
A
->
( ( ) ( )
Subset
of )
equals
:: TEX_4:def 11
union
{
(
MaxADSet
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) where
a
is ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) :
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
}
: ( ( ) ( )
set
) ;
end;
theorem
:: TEX_4:28
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
=
MaxADSet
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:29
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
meets
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
meets
A
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:30
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
meets
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:31
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
MaxADSet
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:32
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of )
c=
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:33
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
MaxADSet
(
MaxADSet
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:34
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
c=
MaxADSet
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
MaxADSet
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:35
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
c=
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
c=
MaxADSet
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
MaxADSet
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:36
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
MaxADSet
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
(
MaxADSet
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
MaxADSet
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:37
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
MaxADSet
(
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
(
MaxADSet
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
MaxADSet
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
cluster
MaxADSet
A
: ( ( non
empty
) ( non
empty
)
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
->
non
empty
;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( (
empty
) (
empty
trivial
proper
boundary
)
Subset
of ) ;
cluster
MaxADSet
A
: ( (
empty
) (
empty
trivial
proper
boundary
)
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
->
empty
;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( non
proper
) ( non
empty
non
proper
)
Subset
of ) ;
cluster
MaxADSet
A
: ( ( non
proper
) ( non
empty
non
proper
)
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
->
non
proper
;
end;
registration
let
Y
be ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) ;
let
A
be ( ( non
trivial
) ( non
empty
non
trivial
)
Subset
of ) ;
cluster
MaxADSet
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
Element
of
bool
the
carrier
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) : ( ( ) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
->
non
trivial
;
end;
theorem
:: TEX_4:38
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
G
,
A
being ( ( ) ( )
Subset
of ) st
G
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:39
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) st
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) )
}
<>
{}
: ( ( ) (
empty
trivial
)
set
) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:40
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
F
,
A
being ( ( ) ( )
Subset
of ) st
F
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:41
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( ) ( )
Subset
of ) st
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) )
}
<>
{}
: ( ( ) (
empty
trivial
)
set
) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
meet
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
begin
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
anti-discrete
means
:: TEX_4:def 12
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
c=
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
anti-discrete
means
:: TEX_4:def 13
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
anti-discrete
means
:: TEX_4:def 14
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) &
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) holds
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Cl
{
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TEX_4:42
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
D
being ( ( ) ( )
Subset
of ) st
D
: ( ( ) ( )
Subset
of ) is
anti-discrete
&
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
D
: ( ( ) ( )
Subset
of ) holds
D
: ( ( ) ( )
Subset
of )
=
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:43
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
( (
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
&
A
: ( ( ) ( )
Subset
of ) is
closed
) iff for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) holds
A
: ( ( ) ( )
Subset
of )
=
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TEX_4:44
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
& not
A
: ( ( ) ( )
Subset
of ) is
open
holds
A
: ( ( ) ( )
Subset
of ) is
boundary
;
theorem
:: TEX_4:45
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
maximal_anti-discrete
;
theorem
:: TEX_4:46
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:47
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
meet
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
F
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:48
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
c=
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:49
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
=
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) iff
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Cl
{
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TEX_4:50
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of )
misses
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
Subset
of ) iff
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
<>
Cl
{
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
:: original:
MaxADSet
redefine
func
MaxADSet
x
->
( ( non
empty
) ( non
empty
)
Subset
of )
equals
:: TEX_4:def 15
(
Cl
{
x
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
/\
(
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
in
G
: ( ( ) ( )
Subset
of ) )
}
)
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
bool
the
carrier
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TEX_4:51
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
Cl
{
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) iff
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
)
c=
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ) ;
theorem
:: TEX_4:52
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
Cl
{
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) iff
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
c=
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ) ;
theorem
:: TEX_4:53
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
misses
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff ( ex
V
being ( ( ) ( )
Subset
of ) st
(
V
: ( ( ) ( )
Subset
of ) is
open
&
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
c=
V
: ( ( ) ( )
Subset
of ) &
V
: ( ( ) ( )
Subset
of )
misses
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) or ex
W
being ( ( ) ( )
Subset
of ) st
(
W
: ( ( ) ( )
Subset
of ) is
open
&
W
: ( ( ) ( )
Subset
of )
misses
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) &
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
c=
W
: ( ( ) ( )
Subset
of ) ) ) ) ;
theorem
:: TEX_4:54
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
misses
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff ( ex
E
being ( ( ) ( )
Subset
of ) st
(
E
: ( ( ) ( )
Subset
of ) is
closed
&
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
c=
E
: ( ( ) ( )
Subset
of ) &
E
: ( ( ) ( )
Subset
of )
misses
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) or ex
F
being ( ( ) ( )
Subset
of ) st
(
F
: ( ( ) ( )
Subset
of ) is
closed
&
F
: ( ( ) ( )
Subset
of )
misses
MaxADSet
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) &
MaxADSet
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
) ( non
empty
)
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) ) ) ) ;
theorem
:: TEX_4:55
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
meet
{
G
: ( ( ) ( )
Subset
of ) where
G
is ( ( ) ( )
Subset
of ) : (
G
: ( ( ) ( )
Subset
of ) is
open
&
A
: ( ( ) ( )
Subset
of )
c=
G
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:56
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
P
being ( ( ) ( )
Subset
of ) st
P
: ( ( ) ( )
Subset
of ) is
open
holds
MaxADSet
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
P
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:57
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
MaxADSet
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:58
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
meet
{
F
: ( ( ) ( )
Subset
of ) where
F
is ( ( ) ( )
Subset
of ) : (
F
: ( ( ) ( )
Subset
of ) is
closed
&
A
: ( ( ) ( )
Subset
of )
c=
F
: ( ( ) ( )
Subset
of ) )
}
: ( ( ) ( )
set
) ;
theorem
:: TEX_4:59
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:60
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
P
being ( ( ) ( )
Subset
of ) st
P
: ( ( ) ( )
Subset
of ) is
closed
holds
MaxADSet
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
P
: ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:61
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
MaxADSet
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:62
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
Cl
(
MaxADSet
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:63
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
MaxADSet
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
MaxADSet
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:64
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
P
,
Q
being ( ( ) ( )
Subset
of ) st (
P
: ( ( ) ( )
Subset
of ) is
closed
or
Q
: ( ( ) ( )
Subset
of ) is
closed
) holds
MaxADSet
(
P
: ( ( ) ( )
Subset
of )
/\
Q
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
(
MaxADSet
P
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
MaxADSet
Q
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TEX_4:65
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
P
,
Q
being ( ( ) ( )
Subset
of ) st (
P
: ( ( ) ( )
Subset
of ) is
open
or
Q
: ( ( ) ( )
Subset
of ) is
open
) holds
MaxADSet
(
P
: ( ( ) ( )
Subset
of )
/\
Q
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
(
MaxADSet
P
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
MaxADSet
Q
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
begin
theorem
:: TEX_4:66
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
Y0
being ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
Y0
: ( ( ) ( )
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
set
) &
Y0
: ( ( ) ( )
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is
anti-discrete
holds
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
;
theorem
:: TEX_4:67
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
Y0
being ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) st
Y0
: ( ( ) ( )
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is
TopSpace-like
holds
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
the
carrier
of
Y0
: ( ( ) ( )
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
set
) &
A
: ( ( ) ( )
Subset
of ) is
anti-discrete
holds
Y0
: ( ( ) ( )
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is
anti-discrete
;
theorem
:: TEX_4:68
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
) ) st ( for
X0
being ( (
open
) (
TopSpace-like
open
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
(
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
misses
X0
: ( (
open
) (
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) or
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
open
) (
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ) ) holds
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
anti-discrete
;
theorem
:: TEX_4:69
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
) ) st ( for
X0
being ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
(
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
misses
X0
: ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) or
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ) ) holds
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
anti-discrete
;
theorem
:: TEX_4:70
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( (
anti-discrete
) (
TopSpace-like
anti-discrete
almost_discrete
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X0
being ( (
open
) (
TopSpace-like
open
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
(
Y0
: ( (
anti-discrete
) (
TopSpace-like
anti-discrete
almost_discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
misses
X0
: ( (
open
) (
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) or
Y0
: ( (
anti-discrete
) (
TopSpace-like
anti-discrete
almost_discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
open
) (
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ) ;
theorem
:: TEX_4:71
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
Y0
being ( (
anti-discrete
) (
TopSpace-like
anti-discrete
almost_discrete
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
X0
being ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
(
Y0
: ( (
anti-discrete
) (
TopSpace-like
anti-discrete
almost_discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
misses
X0
: ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) or
Y0
: ( (
anti-discrete
) (
TopSpace-like
anti-discrete
almost_discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ) ;
definition
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
IT
be ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ;
attr
IT
is
maximal_anti-discrete
means
:: TEX_4:def 16
(
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) is
anti-discrete
& ( for
Y0
being ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) st
Y0
: ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is
anti-discrete
& the
carrier
of
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
c=
the
carrier
of
Y0
: ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
set
) holds
the
carrier
of
IT
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
=
the
carrier
of
Y0
: ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
set
) ) );
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
cluster
maximal_anti-discrete
->
anti-discrete
for ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
cluster
non
anti-discrete
->
non
maximal_anti-discrete
for ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
end;
theorem
:: TEX_4:72
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
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of )
=
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
) holds
(
Y0
: ( ( non
empty
) ( non
empty
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
maximal_anti-discrete
iff
A
: ( ( ) ( )
Subset
of ) is
maximal_anti-discrete
) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
open
anti-discrete
->
non
empty
maximal_anti-discrete
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
open
non
maximal_anti-discrete
->
non
empty
non
anti-discrete
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
anti-discrete
non
maximal_anti-discrete
->
non
empty
non
open
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
closed
anti-discrete
->
non
empty
maximal_anti-discrete
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
closed
non
maximal_anti-discrete
->
non
empty
non
anti-discrete
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
cluster
non
empty
anti-discrete
non
maximal_anti-discrete
->
non
empty
non
closed
for ( ( ) ( )
SubSpace
of
X
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) ;
end;
definition
let
Y
be ( ( ) ( )
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ;
func
MaxADSspace
x
->
( (
strict
) (
strict
)
SubSpace
of
Y
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) )
means
:: TEX_4:def 17
the
carrier
of
it
: ( ( ) ( )
Element
of
Y
: ( ( non
empty
TopSpace-like
almost_discrete
) ( non
empty
TopSpace-like
almost_discrete
)
TopStruct
) ) : ( ( ) ( )
set
)
=
MaxADSet
x
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Subset
of ) ;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
MaxADSspace
x
: ( ( ) ( )
Element
of the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
)
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
->
non
empty
strict
;
end;
theorem
:: TEX_4:73
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
Sspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
strict
) ( non
empty
trivial
V46
()
V51
(1 : ( ( ) ( non
empty
)
set
) )
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is ( ( ) ( )
SubSpace
of
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ) ;
theorem
:: TEX_4:74
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) iff
TopStruct
(# the
carrier
of
(
MaxADSspace
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
) ) ;
theorem
:: TEX_4:75
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
( the
carrier
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
misses
the
carrier
of
(
MaxADSspace
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) or
TopStruct
(# the
carrier
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
(
MaxADSspace
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
3
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
) ) ;
registration
let
X
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
strict
TopSpace-like
maximal_anti-discrete
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
) ;
let
x
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
MaxADSspace
x
: ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) )
->
strict
maximal_anti-discrete
;
end;
theorem
:: TEX_4:76
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( ( non
empty
closed
) ( non
empty
TopSpace-like
closed
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
TopSpace-like
anti-discrete
almost_discrete
maximal_anti-discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( ( non
empty
closed
) ( non
empty
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
theorem
:: TEX_4:77
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
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
TopSpace-like
anti-discrete
almost_discrete
maximal_anti-discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( ( non
empty
open
) ( non
empty
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
theorem
:: TEX_4:78
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
Cl
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V170
(
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
Sspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( non
empty
strict
) ( non
empty
trivial
V46
()
V51
(1 : ( ( ) ( non
empty
)
set
) )
strict
TopSpace-like
V160
()
anti-discrete
almost_discrete
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is
maximal_anti-discrete
;
notation
let
Y
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
synonym
Sspace
A
for
Y
|
A
;
end;
theorem
:: TEX_4:79
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:80
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
Y0
being ( ( ) ( )
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) holds
Sspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is ( ( ) ( )
SubSpace
of
Y0
: ( ( ) ( )
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ) ;
registration
let
Y
be ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) ;
cluster
strict
non
proper
for ( ( ) ( )
SubSpace
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) ) ;
end;
registration
let
Y
be ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) ;
let
A
be ( ( non
trivial
) ( non
empty
non
trivial
)
Subset
of ) ;
cluster
Sspace
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
Element
of
bool
the
carrier
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) : ( ( ) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) )
->
non
trivial
strict
;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( non
proper
) ( non
empty
non
proper
)
Subset
of ) ;
cluster
Sspace
A
: ( ( non
proper
) ( non
empty
non
proper
)
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
->
strict
non
proper
;
end;
definition
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
func
MaxADSspace
A
->
( (
strict
) (
strict
)
SubSpace
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) )
means
:: TEX_4:def 18
the
carrier
of
it
: ( ( ) ( )
Element
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) ) : ( ( ) ( )
set
)
=
MaxADSet
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Subset
of ) ;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( non
empty
) ( non
empty
)
Subset
of ) ;
cluster
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
)
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
->
non
empty
strict
;
end;
theorem
:: TEX_4:81
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) ;
theorem
:: TEX_4:82
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
Sspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is ( ( ) ( )
SubSpace
of
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ) ;
theorem
:: TEX_4:83
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
TopStruct
(# the
carrier
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
(
MaxADSspace
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
{
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
) ;
theorem
:: TEX_4:84
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is ( ( ) ( )
SubSpace
of
MaxADSspace
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ) ;
theorem
:: TEX_4:85
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
TopStruct
(# the
carrier
of
(
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
2
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
(
MaxADSspace
(
MaxADSet
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
(
MaxADSet
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
(
MaxADSet
b
2
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
) ;
theorem
:: TEX_4:86
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) holds
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) is ( ( ) ( )
SubSpace
of
MaxADSspace
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) ) ;
theorem
:: TEX_4:87
for
Y
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
( (
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) &
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) ) iff
TopStruct
(# the
carrier
of
(
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
2
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
)
=
TopStruct
(# the
carrier
of
(
MaxADSspace
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
) , the
topology
of
(
MaxADSspace
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( )
Element
of
bool
(
bool
the
carrier
of
(
MaxADSspace
b
3
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
)
SubSpace
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) ) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopStruct
) ) ;
registration
let
Y
be ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) ;
let
A
be ( ( non
trivial
) ( non
empty
non
trivial
)
Subset
of ) ;
cluster
MaxADSspace
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
Element
of
bool
the
carrier
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) : ( ( ) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
Y
: ( ( non
trivial
) ( non
empty
non
trivial
)
TopStruct
) )
->
non
trivial
strict
;
end;
registration
let
Y
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
let
A
be ( ( non
proper
) ( non
empty
non
proper
)
Subset
of ) ;
cluster
MaxADSspace
A
: ( ( non
proper
) ( non
empty
non
proper
)
Element
of
bool
the
carrier
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
)
SubSpace
of
Y
: ( ( non
empty
) ( non
empty
)
TopStruct
) )
->
strict
non
proper
;
end;
theorem
:: TEX_4:88
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( (
open
) (
TopSpace-like
open
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) holds
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
open
) (
TopSpace-like
open
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;
theorem
:: TEX_4:89
for
X
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
X0
being ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
X
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) )
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( )
Subset
of ) holds
MaxADSspace
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) is ( ( ) (
TopSpace-like
)
SubSpace
of
X0
: ( (
closed
) (
TopSpace-like
closed
)
SubSpace
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) ) ;