:: CLOSURE3 semantic presentation
begin
registration
let
S
be ( ( non
empty
) ( non
empty
)
1-sorted
) ;
cluster
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
1-sorted
) : ( ( ) ( non
empty
)
set
) #) : ( (
strict
) (
strict
)
1-sorted
)
->
strict
non
empty
;
end;
theorem
:: CLOSURE3:1
for
I
being ( ( non
empty
) ( non
empty
)
set
)
for
M
,
N
being ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) holds
M
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
+*
N
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
=
N
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ;
theorem
:: CLOSURE3:2
for
I
being ( ( ) ( )
set
)
for
M
,
N
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
F
being ( ( ) (
functional
)
SubsetFamily
of ) st
N
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
F
: ( ( ) (
functional
)
SubsetFamily
of ) holds
meet
|:
F
: ( ( ) (
functional
)
SubsetFamily
of )
:|
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
bool
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
set
) ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
c='
N
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: CLOSURE3:3
for
S
being ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
)
for
MA
being ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) )
for
F
being ( ( ) (
functional
)
SubsetFamily
of ) st
F
: ( ( ) (
functional
)
SubsetFamily
of )
c=
SubSort
MA
: ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) : ( ( ) ( )
set
) holds
for
B
being ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
MSSubset
of
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) st
B
: ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
MSSubset
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) )
=
meet
|:
F
: ( ( ) (
functional
)
SubsetFamily
of )
:|
: ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
ManySortedSubset
of
bool
the
Sorts
of
b
2
: ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) : ( (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
non-empty
non
empty-yielding
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
set
) ) : ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
ManySortedSubset
of the
Sorts
of
b
2
: ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) : ( (
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
non-empty
non
empty-yielding
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
set
) ) holds
B
: ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V17
( the
carrier
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) ) )
MSSubset
of
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) is
opers_closed
;
begin
theorem
:: CLOSURE3:4
for
A
,
B
,
C
being ( ( ) ( )
set
) st
A
: ( ( ) ( )
set
)
is_coarser_than
B
: ( ( ) ( )
set
) &
B
: ( ( ) ( )
set
)
is_coarser_than
C
: ( ( ) ( )
set
) holds
A
: ( ( ) ( )
set
)
is_coarser_than
C
: ( ( ) ( )
set
) ;
definition
let
I
be ( ( non
empty
) ( non
empty
)
set
) ;
let
M
be ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) ;
:: original:
support
redefine
func
support
M
->
( ( ) ( )
set
)
equals
:: CLOSURE3:def 1
{
x
: ( ( ) ( )
Element
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of
I
: ( ( ) ( )
set
) ) :
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
.
x
: ( ( ) ( )
Element
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Function-like
functional
finite
V45
()
V87
() )
set
)
}
;
end;
theorem
:: CLOSURE3:5
for
I
being ( ( non
empty
) ( non
empty
)
set
)
for
M
being ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) holds
M
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
=
(
[[0]]
I
: ( ( non
empty
) ( non
empty
)
set
)
)
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
non
non-empty
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
+*
(
M
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
|
(
support
M
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Function-like
)
set
) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) ;
theorem
:: CLOSURE3:6
for
I
being ( ( non
empty
) ( non
empty
)
set
)
for
M1
,
M2
being ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) st
M1
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
|
(
support
M1
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
)
=
M2
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
|
(
support
M2
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Function-like
)
set
) holds
M1
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
=
M2
: ( (
Relation-like
V8
()
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
V8
() non
empty-yielding
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ;
theorem
:: CLOSURE3:7
canceled;
theorem
:: CLOSURE3:8
for
I
being ( ( non
empty
) ( non
empty
)
set
)
for
M
being ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
for
x
being ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
i
being ( ( ) ( )
Element
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
for
y
being ( ( ) ( )
set
) st
y
: ( ( ) ( )
set
)
in
x
: ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
i
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
) holds
ex
a
being ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) st
(
y
: ( ( ) ( )
set
)
in
a
: ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
i
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
) &
a
: ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) is
V42
() &
support
a
: ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) is
finite
&
a
: ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
c=
x
: ( ( ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
b
2
: ( (
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
definition
let
I
be ( ( ) ( )
set
) ;
let
M
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
let
A
be ( ( ) (
functional
)
SubsetFamily
of ) ;
func
MSUnion
A
->
( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) )
means
:: CLOSURE3:def 2
for
i
being ( ( ) ( )
set
) st
i
: ( ( ) ( )
set
)
in
I
: ( ( ) ( )
set
) holds
it
: ( (
Function-like
quasi_total
) (
Relation-like
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
-defined
I
: ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) ,
I
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
.
i
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
union
{
(
f
: ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.
i
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) where
f
is ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) :
f
: ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
in
A
: ( ( ) (
functional
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( )
set
) ;
end;
registration
let
I
be ( ( ) ( )
set
) ;
let
M
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
let
A
be ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
SubsetFamily
of ) ;
cluster
MSUnion
A
: ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) )
->
V9
() ;
end;
theorem
:: CLOSURE3:9
for
I
being ( ( ) ( )
set
)
for
M
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
A
being ( ( ) (
functional
)
SubsetFamily
of ) holds
MSUnion
A
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
=
union
|:
A
: ( ( ) (
functional
)
SubsetFamily
of )
:|
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
bool
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
definition
let
I
be ( ( ) ( )
set
) ;
let
M
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
let
A
,
B
be ( ( ) (
functional
)
SubsetFamily
of ) ;
:: original:
\/
redefine
func
A
\/
B
->
( ( ) (
functional
)
SubsetFamily
of ) ;
end;
theorem
:: CLOSURE3:10
for
I
being ( ( ) ( )
set
)
for
M
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
A
,
B
being ( ( ) (
functional
)
SubsetFamily
of ) holds
MSUnion
(
A
: ( ( ) (
functional
)
SubsetFamily
of )
\/
B
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
=
(
MSUnion
A
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
\/
(
MSUnion
B
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: CLOSURE3:11
for
I
being ( ( ) ( )
set
)
for
M
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
A
,
B
being ( ( ) (
functional
)
SubsetFamily
of ) st
A
: ( ( ) (
functional
)
SubsetFamily
of )
c=
B
: ( ( ) (
functional
)
SubsetFamily
of ) holds
MSUnion
A
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
c=
MSUnion
B
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) ;
definition
let
I
be ( ( ) ( )
set
) ;
let
M
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
let
A
,
B
be ( ( ) (
functional
)
SubsetFamily
of ) ;
:: original:
/\
redefine
func
A
/\
B
->
( ( ) (
functional
)
SubsetFamily
of ) ;
end;
theorem
:: CLOSURE3:12
for
I
being ( ( ) ( )
set
)
for
M
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
A
,
B
being ( ( ) (
functional
)
SubsetFamily
of ) holds
MSUnion
(
A
: ( ( ) (
functional
)
SubsetFamily
of )
/\
B
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
c=
(
MSUnion
A
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
/\
(
MSUnion
B
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: CLOSURE3:13
for
I
being ( ( ) ( )
set
)
for
M
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
AA
being ( ( ) ( )
set
) st ( for
x
being ( ( ) ( )
set
) st
x
: ( ( ) (
functional
)
SubsetFamily
of )
in
AA
: ( ( ) ( )
set
) holds
x
: ( ( ) (
functional
)
SubsetFamily
of ) is ( ( ) (
functional
)
SubsetFamily
of ) ) holds
for
A
,
B
being ( ( ) (
functional
)
SubsetFamily
of ) st
B
: ( ( ) (
functional
)
SubsetFamily
of )
=
{
(
MSUnion
X
: ( ( ) (
functional
)
SubsetFamily
of )
)
: ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) where
X
is ( ( ) (
functional
)
SubsetFamily
of ) :
X
: ( ( ) (
functional
)
SubsetFamily
of )
in
AA
: ( ( ) ( )
set
)
}
&
A
: ( ( ) (
functional
)
SubsetFamily
of )
=
union
AA
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
MSUnion
B
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) )
=
MSUnion
A
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
b
2
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) ;
begin
definition
let
I
be ( ( non
empty
) ( non
empty
)
set
) ;
let
M
be ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) ;
let
S
be ( (
Function-like
quasi_total
) ( non
empty
Relation-like
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
-defined
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V17
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
)
SetOp
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) ;
attr
S
is
algebraic
means
:: CLOSURE3:def 3
for
x
being ( ( ) ( non
empty
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) st
x
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
=
S
: ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
.
x
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
A
being ( ( ) (
functional
)
SubsetFamily
of ) st
(
A
: ( ( ) (
functional
)
SubsetFamily
of )
=
{
(
S
: ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
.
a
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) where
a
is ( ( ) ( non
empty
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : (
a
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) is
V42
() &
support
a
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) is
finite
&
a
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
c=
x
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
}
&
x
: ( ( ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
=
MSUnion
A
: ( ( ) (
functional
)
SubsetFamily
of ) : ( ( ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
ManySortedSubset
of
M
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V17
(
I
: ( ( ) ( )
set
) ) )
set
) ) );
end;
registration
let
I
be ( ( non
empty
) ( non
empty
)
set
) ;
let
M
be ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
ManySortedSet
of
I
: ( ( non
empty
) ( non
empty
)
set
) ) ;
cluster
non
empty
Relation-like
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
-defined
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V17
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
reflexive
monotonic
idempotent
algebraic
for ( ( ) ( )
Element
of
bool
[:
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
M
: ( (
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
I
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
I
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
S
be ( ( non
empty
) ( non
empty
)
1-sorted
) ;
let
IT
be ( (
absolutely-multiplicative
) (
multiplicative
absolutely-multiplicative
properly-upper-bound
)
ClosureSystem
of
S
: ( ( non
empty
) ( non
empty
)
1-sorted
) ) ;
attr
IT
is
algebraic
means
:: CLOSURE3:def 4
ClSys->ClOp
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Function-like
quasi_total
reflexive
monotonic
idempotent
) ( non
empty
Relation-like
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
-defined
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V17
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
) : ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) )
quasi_total
reflexive
monotonic
idempotent
)
Element
of
bool
[:
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( (
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
) ( non
empty
functional
with_common_domain
additive
absolutely-additive
multiplicative
absolutely-multiplicative
properly-upper-bound
properly-lower-bound
)
Element
of
bool
(
Bool
the
Sorts
of
IT
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
algebraic
;
end;
definition
let
S
be ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ;
let
MA
be ( (
non-empty
) (
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) ;
func
SubAlgCl
MA
->
( (
strict
) (
strict
)
ClosureStr
over
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) )
means
:: CLOSURE3:def 5
( the
Sorts
of
it
: ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
Element
of
bool
(
Bool
MA
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
Relation-like
the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
) ) )
set
)
=
the
Sorts
of
MA
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
set
) & the
Family
of
it
: ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
Element
of
bool
(
Bool
MA
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Element
of
bool
(
Bool
the
Sorts
of
it
: ( (
empty
) (
empty
proper
Function-like
functional
finite
V45
()
V87
() )
Element
of
bool
(
Bool
MA
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
Relation-like
the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
)
-defined
Function-like
V17
( the
carrier
of
1-sorted
(# the
carrier
of
S
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) #) : ( (
strict
) (
strict
)
1-sorted
) : ( ( ) ( )
set
) ) )
set
)
)
: ( ( ) ( non
empty
functional
with_common_domain
)
set
) : ( ( ) ( non
empty
)
set
) )
=
SubSort
MA
: ( (
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) ) ( non
empty
Relation-like
S
: ( ( non
empty
) ( non
empty
)
set
)
-defined
Function-like
V17
(
S
: ( ( non
empty
) ( non
empty
)
set
) ) )
set
) : ( ( ) ( )
set
) );
end;
theorem
:: CLOSURE3:14
for
S
being ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
)
for
MA
being ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) holds
SubSort
MA
: ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
b
1
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) : ( ( ) ( )
set
) is ( (
absolutely-multiplicative
) ( non
empty
functional
multiplicative
absolutely-multiplicative
properly-upper-bound
)
SubsetFamily
of ) ;
registration
let
S
be ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ;
let
MA
be ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) ;
cluster
SubAlgCl
MA
: ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) : ( (
strict
) (
strict
)
ClosureStr
over
1-sorted
(# the
carrier
of
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) #) : ( (
strict
) (
strict
non
empty
)
1-sorted
) )
->
strict
absolutely-multiplicative
;
end;
registration
let
S
be ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ;
let
MA
be ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) ;
cluster
SubAlgCl
MA
: ( (
strict
non-empty
) (
strict
non-empty
)
MSAlgebra
over
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) ) : ( (
strict
) (
strict
multiplicative
absolutely-multiplicative
properly-upper-bound
)
ClosureStr
over
1-sorted
(# the
carrier
of
S
: ( ( non
empty
non
void
) ( non
empty
non
void
V62
() )
ManySortedSign
) : ( ( ) ( non
empty
)
set
) #) : ( (
strict
) (
strict
non
empty
)
1-sorted
) )
->
strict
algebraic
;
end;