:: ISOMICHI semantic presentation
begin
registration
let
D
be ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ;
cluster
ADTS
D
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
strict
TopSpace-like
anti-discrete
)
TopStruct
)
->
non
trivial
;
end;
registration
cluster
non
trivial
strict
TopSpace-like
anti-discrete
for ( ( ) ( )
TopStruct
) ;
end;
theorem
:: ISOMICHI:1
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
(
Int
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
/\
(
Int
(
Cl
(
Int
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Int
(
Cl
(
Int
(
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:2
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
Cl
(
Int
(
Cl
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
(
Cl
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
\/
(
Cl
(
Int
(
Cl
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
begin
definition
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
supercondensed
means
:: ISOMICHI:def 1
Int
(
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
attr
A
is
subcondensed
means
:: ISOMICHI:def 2
Cl
(
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
closed
->
supercondensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:3
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
closed
holds
A
: ( ( ) ( )
Subset
of ) is
supercondensed
;
theorem
:: ISOMICHI:4
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
open
holds
A
: ( ( ) ( )
Subset
of ) is
subcondensed
;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
attr
A
is
condensed
means
:: ISOMICHI:def 3
(
Cl
(
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) &
Int
(
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) );
end;
theorem
:: ISOMICHI:5
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
condensed
iff (
A
: ( ( ) ( )
Subset
of ) is
subcondensed
&
A
: ( ( ) ( )
Subset
of ) is
supercondensed
) ) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
condensed
->
supercondensed
subcondensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
supercondensed
subcondensed
->
condensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
condensed
supercondensed
subcondensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:6
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
supercondensed
holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
subcondensed
;
theorem
:: ISOMICHI:7
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
subcondensed
holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
supercondensed
;
theorem
:: ISOMICHI:8
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
supercondensed
iff
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: ISOMICHI:9
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
subcondensed
iff
A
: ( ( ) ( )
Subset
of )
c=
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
subcondensed
->
semi-open
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
semi-open
->
subcondensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:10
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
condensed
iff (
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
c=
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;
begin
notation
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
synonym
regular_open
A
for
open_condensed
;
end;
notation
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
synonym
regular_closed
A
for
closed_condensed
;
end;
theorem
:: ISOMICHI:11
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
(
[#]
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
proper
open
closed
dense
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_open
&
[#]
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( non
proper
open
closed
dense
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_closed
) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
[#]
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( non
proper
open
closed
dense
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
regular_closed
regular_open
;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
empty
->
regular_closed
regular_open
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:12
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) holds
Int
(
Cl
(
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
)
: ( ( ) (
empty
trivial
V65
()
V66
()
V67
()
V68
()
V69
()
V70
()
V71
()
open
closed
boundary
nowhere_dense
regular_closed
regular_open
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
{}
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) (
empty
trivial
V65
()
V66
()
V67
()
V68
()
V69
()
V70
()
V71
()
open
closed
boundary
nowhere_dense
regular_closed
regular_open
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:13
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
regular_open
holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_closed
;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
regular_closed
regular_open
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
regular_open
) (
regular_open
)
Subset
of ) ;
cluster
A
: ( (
regular_open
) (
regular_open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
regular_closed
;
end;
theorem
:: ISOMICHI:14
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
regular_closed
holds
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_open
;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
regular_closed
) (
regular_closed
)
Subset
of ) ;
cluster
A
: ( (
regular_closed
) (
regular_closed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
regular_open
;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
regular_open
->
open
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
regular_closed
->
closed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:15
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_open
&
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_closed
) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
cluster
Int
(
Cl
A
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
regular_open
;
cluster
Cl
(
Int
A
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
regular_closed
;
end;
theorem
:: ISOMICHI:16
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
regular_open
iff (
A
: ( ( ) ( )
Subset
of ) is
supercondensed
&
A
: ( ( ) ( )
Subset
of ) is
open
) ) ;
theorem
:: ISOMICHI:17
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
regular_closed
iff (
A
: ( ( ) ( )
Subset
of ) is
subcondensed
&
A
: ( ( ) ( )
Subset
of ) is
closed
) ) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
regular_open
->
open
condensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
open
condensed
->
regular_open
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
regular_closed
->
closed
condensed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
closed
condensed
->
regular_closed
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:18
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
condensed
iff ex
B
being ( ( ) ( )
Subset
of ) st
(
B
: ( ( ) ( )
Subset
of ) is
regular_open
&
B
: ( ( ) ( )
Subset
of )
c=
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
c=
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: ISOMICHI:19
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
condensed
iff ex
B
being ( ( ) ( )
Subset
of ) st
(
B
: ( ( ) ( )
Subset
of ) is
regular_closed
&
Int
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
Subset
of ) &
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) ) ) ;
begin
definition
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
redefine
func
Fr
A
equals
:: ISOMICHI:def 4
(
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
\
(
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:20
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
condensed
iff (
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
\
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) &
Fr
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
/\
(
Cl
(
Int
(
A
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ) ;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
func
Border
A
->
( ( ) ( )
Subset
of )
equals
:: ISOMICHI:def 5
Int
(
Fr
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:21
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) is
regular_open
&
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
\
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) &
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
/\
(
Int
(
Cl
(
A
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
cluster
Border
A
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
->
regular_open
;
end;
theorem
:: ISOMICHI:22
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
supercondensed
iff (
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_open
&
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Subset
of ) is
empty
) ) ;
theorem
:: ISOMICHI:23
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
subcondensed
iff (
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_closed
&
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Subset
of ) is
empty
) ) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
cluster
Border
(
Border
A
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Subset
of ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Subset
of )
->
empty
;
end;
theorem
:: ISOMICHI:24
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
condensed
iff (
Int
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_open
&
Cl
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
regular_closed
&
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Subset
of ) is
empty
) ) ;
begin
theorem
:: ISOMICHI:25
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.]
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) holds
Int
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:26
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
[.
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
+infty
: ( ( ) ( non
empty
ext-real
positive
non
negative
non
real
)
set
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) holds
Int
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
].
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
+infty
: ( ( ) ( non
empty
ext-real
positive
non
negative
non
real
)
set
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:27
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
,
b
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
(
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.]
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
(
IRRAT
(
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) )
)
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
[.
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
+infty
: ( ( ) ( non
empty
ext-real
positive
non
negative
non
real
)
set
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) holds
Cl
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
closed
supercondensed
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) ;
theorem
:: ISOMICHI:28
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
,
b
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
RAT
(
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) holds
Int
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
{}
: ( ( ) (
empty
trivial
V65
()
V66
()
V67
()
V68
()
V69
()
V70
()
V71
() )
set
) ;
theorem
:: ISOMICHI:29
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
,
b
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
IRRAT
(
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) holds
Int
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
{}
: ( ( ) (
empty
trivial
V65
()
V66
()
V67
()
V68
()
V69
()
V70
()
V71
() )
set
) ;
theorem
:: ISOMICHI:30
for
a
,
b
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
>=
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) holds
IRRAT
(
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
=
{}
: ( ( ) (
empty
trivial
V65
()
V66
()
V67
()
V68
()
V69
()
V70
()
V71
() )
set
) ;
theorem
:: ISOMICHI:31
for
a
,
b
being ( (
real
) (
ext-real
V51
()
real
)
number
) holds
IRRAT
(
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
c=
[.
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
+infty
: ( ( ) ( non
empty
ext-real
positive
non
negative
non
real
)
set
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:32
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
,
b
,
c
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
(
RAT
(
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
c
: ( (
real
) (
ext-real
V51
()
real
)
number
) )
)
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) &
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
<
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) &
b
: ( (
real
) (
ext-real
V51
()
real
)
number
)
<
c
: ( (
real
) (
ext-real
V51
()
real
)
number
) holds
Int
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:33
for
a
,
b
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
<
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) holds
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
)
=
(
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
[.
a
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
b
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.]
: ( ( ) (
V65
()
V66
()
V67
()
closed
)
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
].
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
+infty
: ( ( ) ( non
empty
ext-real
positive
non
negative
non
real
)
set
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: ISOMICHI:34
for
A
being ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
for
a
,
b
,
c
being ( (
real
) (
ext-real
V51
()
real
)
number
) st
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of )
=
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.]
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
[.
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
c
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.]
: ( ( ) (
V65
()
V66
()
V67
()
closed
)
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) &
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
<
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) &
b
: ( (
real
) (
ext-real
V51
()
real
)
number
)
<
c
: ( (
real
) (
ext-real
V51
()
real
)
number
) holds
Int
A
: ( ( ) (
V65
()
V66
()
V67
() )
Subset
of ) : ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
the
carrier
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
V167
() )
TopStruct
) : ( ( ) ( non
empty
V65
()
V66
()
V67
() )
set
) : ( ( ) ( )
set
) )
=
].
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
non
real
)
set
) ,
a
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.[
: ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) )
\/
].
b
: ( (
real
) (
ext-real
V51
()
real
)
number
) ,
c
: ( (
real
) (
ext-real
V51
()
real
)
number
)
.[
: ( ( ) (
V65
()
V66
()
V67
()
open
)
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
V65
()
V66
()
V67
() )
Element
of
bool
REAL
: ( ( ) (
V65
()
V66
()
V67
()
V71
() )
set
) : ( ( ) ( )
set
) ) ;
begin
notation
let
A
,
B
be ( ( ) ( )
set
) ;
antonym
A
,
B
are_c=-incomparable
for
A
,
B
are_c=-comparable
;
end;
theorem
:: ISOMICHI:35
for
A
,
B
being ( ( ) ( )
set
) holds
(
A
: ( ( ) ( )
set
) ,
B
: ( ( ) ( )
set
)
are_c=-incomparable
or
A
: ( ( ) ( )
set
)
c=
B
: ( ( ) ( )
set
) or
B
: ( ( ) ( )
set
)
c<
A
: ( ( ) ( )
set
) ) ;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
attr
A
is
1st_class
means
:: ISOMICHI:def 6
Int
(
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
c=
Cl
(
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
attr
A
is
2nd_class
means
:: ISOMICHI:def 7
Cl
(
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
c<
Int
(
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
attr
A
is
3rd_class
means
:: ISOMICHI:def 8
Cl
(
Int
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ,
Int
(
Cl
A
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
)
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
are_c=-incomparable
;
end;
theorem
:: ISOMICHI:36
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
1st_class
or
A
: ( ( ) ( )
Subset
of ) is
2nd_class
or
A
: ( ( ) ( )
Subset
of ) is
3rd_class
) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
1st_class
->
non
2nd_class
non
3rd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
2nd_class
->
non
1st_class
non
3rd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
3rd_class
->
non
1st_class
non
2nd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:37
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
1st_class
iff
Border
A
: ( ( ) ( )
Subset
of ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
)
Subset
of ) is
empty
) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
supercondensed
->
1st_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
cluster
subcondensed
->
1st_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
definition
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
attr
T
is
with_1st_class_subsets
means
:: ISOMICHI:def 9
ex
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
1st_class
;
attr
T
is
with_2nd_class_subsets
means
:: ISOMICHI:def 10
ex
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
2nd_class
;
attr
T
is
with_3rd_class_subsets
means
:: ISOMICHI:def 11
ex
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
3rd_class
;
end;
registration
let
T
be ( ( non
empty
TopSpace-like
anti-discrete
) ( non
empty
TopSpace-like
anti-discrete
)
TopSpace
) ;
cluster
non
empty
proper
->
2nd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
T
be ( ( non
trivial
strict
TopSpace-like
anti-discrete
) ( non
empty
non
trivial
strict
TopSpace-like
anti-discrete
)
TopSpace
) ;
cluster
2nd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
trivial
strict
TopSpace-like
anti-discrete
) ( non
empty
non
trivial
strict
TopSpace-like
anti-discrete
)
TopStruct
) : ( ( ) ( non
empty
non
trivial
)
set
) : ( ( ) ( )
set
) ) ;
end;
registration
cluster
non
trivial
strict
TopSpace-like
with_1st_class_subsets
with_2nd_class_subsets
for ( ( ) ( )
TopStruct
) ;
cluster
non
empty
strict
TopSpace-like
with_3rd_class_subsets
for ( ( ) ( )
TopStruct
) ;
end;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
cluster
1st_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
with_2nd_class_subsets
) (
TopSpace-like
with_2nd_class_subsets
)
TopSpace
) ;
cluster
2nd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
with_2nd_class_subsets
) (
TopSpace-like
with_2nd_class_subsets
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
T
be ( (
TopSpace-like
with_3rd_class_subsets
) (
TopSpace-like
with_3rd_class_subsets
)
TopSpace
) ;
cluster
3rd_class
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
with_3rd_class_subsets
) (
TopSpace-like
with_3rd_class_subsets
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: ISOMICHI:38
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
1st_class
iff
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
1st_class
) ;
theorem
:: ISOMICHI:39
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
2nd_class
iff
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
2nd_class
) ;
theorem
:: ISOMICHI:40
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of ) is
3rd_class
iff
A
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
3rd_class
) ;
registration
let
T
be ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ;
let
A
be ( (
1st_class
) (
1st_class
non
2nd_class
non
3rd_class
)
Subset
of ) ;
cluster
A
: ( (
1st_class
) (
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
) (
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
1st_class
;
end;
registration
let
T
be ( (
TopSpace-like
with_2nd_class_subsets
) (
TopSpace-like
with_2nd_class_subsets
)
TopSpace
) ;
let
A
be ( (
2nd_class
) ( non
1st_class
2nd_class
non
3rd_class
)
Subset
of ) ;
cluster
A
: ( (
2nd_class
) ( non
1st_class
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
with_2nd_class_subsets
) (
TopSpace-like
with_2nd_class_subsets
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
with_2nd_class_subsets
) (
TopSpace-like
with_2nd_class_subsets
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
2nd_class
;
end;
registration
let
T
be ( (
TopSpace-like
with_3rd_class_subsets
) (
TopSpace-like
with_3rd_class_subsets
)
TopSpace
) ;
let
A
be ( (
3rd_class
) ( non
1st_class
non
2nd_class
3rd_class
)
Subset
of ) ;
cluster
A
: ( (
3rd_class
) ( non
1st_class
non
2nd_class
3rd_class
)
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
with_3rd_class_subsets
) (
TopSpace-like
with_3rd_class_subsets
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
`
: ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( (
TopSpace-like
with_3rd_class_subsets
) (
TopSpace-like
with_3rd_class_subsets
)
TopStruct
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
->
3rd_class
;
end;
theorem
:: ISOMICHI:41
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
1st_class
holds
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Int
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) &
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Cl
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: ISOMICHI:42
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
being ( ( ) ( )
Subset
of ) st (
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Int
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) or
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Cl
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) holds
A
: ( ( ) ( )
Subset
of ) is
1st_class
;
theorem
:: ISOMICHI:43
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
1st_class
&
B
: ( ( ) ( )
Subset
of ) is
1st_class
holds
(
(
Int
(
Cl
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
/\
(
Int
(
Cl
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Int
(
Cl
(
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
open
condensed
regular_open
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) &
(
Cl
(
Int
A
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
\/
(
Cl
(
Int
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
supercondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
Cl
(
Int
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) (
closed
condensed
regular_closed
semi-open
supercondensed
subcondensed
1st_class
non
2nd_class
non
3rd_class
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: ISOMICHI:44
for
T
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
A
,
B
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
1st_class
&
B
: ( ( ) ( )
Subset
of ) is
1st_class
holds
(
A
: ( ( ) ( )
Subset
of )
\/
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
1st_class
&
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ) is
1st_class
) ;