:: MBOOLEAN semantic presentation
begin
definition
let
I
be ( ( ) ( )
set
) ;
let
A
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
func
bool
A
->
( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
means
:: MBOOLEAN:def 1
for
i
being ( ( ) ( )
set
) st
i
: ( ( ) ( )
set
)
in
I
: ( ( ) ( )
set
) holds
it
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) )
Function-yielding
) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) )
Function-yielding
V22
() )
set
)
.
i
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
Function-like
)
set
)
=
bool
(
A
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
set
)
.
i
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ;
end;
registration
let
I
be ( ( ) ( )
set
) ;
let
A
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
cluster
bool
A
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
->
Relation-like
V2
()
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ;
end;
theorem
:: MBOOLEAN:1
for
I
being ( ( ) ( )
set
)
for
X
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
bool
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) iff for
A
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) iff
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) ) ;
theorem
:: MBOOLEAN:2
for
I
being ( ( ) ( )
set
) holds
bool
(
[[0]]
I
: ( ( ) ( )
set
)
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
I
: ( ( ) ( )
set
)
-->
{
{}
: ( ( ) (
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
) : ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
{}
: ( ( ) (
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) ;
theorem
:: MBOOLEAN:3
for
I
,
x
being ( ( ) ( )
set
) holds
bool
(
I
: ( ( ) ( )
set
)
-->
x
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
I
: ( ( ) ( )
set
)
-->
(
bool
x
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
) : ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
(
bool
b
2
: ( ( ) ( )
set
)
)
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) ;
theorem
:: MBOOLEAN:4
for
I
,
x
being ( ( ) ( )
set
) holds
bool
(
I
: ( ( ) ( )
set
)
-->
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
I
: ( ( ) ( )
set
)
-->
{
{}
: ( ( ) (
empty
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
) : ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
{}
: ( ( ) (
empty
)
set
) ,
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) ;
theorem
:: MBOOLEAN:5
for
I
being ( ( ) ( )
set
)
for
A
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
[[0]]
I
: ( ( ) ( )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:6
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
bool
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:7
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
(
bool
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
bool
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:8
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
(
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
(
bool
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
=
bool
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
for
i
being ( ( ) ( )
set
) st
i
: ( ( ) ( )
set
)
in
I
: ( ( ) ( )
set
) holds
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
.
i
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ,
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
.
i
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
are_c=-comparable
;
theorem
:: MBOOLEAN:9
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
bool
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
(
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
(
bool
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:10
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
bool
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
(
I
: ( ( ) ( )
set
)
-->
{
{}
: ( ( ) (
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
{}
: ( ( ) (
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ))
\/
(
(
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\
(
bool
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:11
for
I
being ( ( ) ( )
set
)
for
X
,
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) iff (
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) &
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
misses
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) ) ;
theorem
:: MBOOLEAN:12
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
bool
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
(
bool
(
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
bool
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\+\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:13
for
I
being ( ( ) ( )
set
)
for
X
,
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\+\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) iff (
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) &
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
misses
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ) ) ;
theorem
:: MBOOLEAN:14
for
I
being ( ( ) ( )
set
)
for
X
,
A
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st (
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) or
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:15
for
I
being ( ( ) ( )
set
)
for
X
,
A
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:16
for
I
being ( ( ) ( )
set
)
for
X
,
A
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) &
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\+\
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:17
for
I
being ( ( ) ( )
set
)
for
X
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
[|
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ,
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
|]
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
bool
(
bool
(
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:18
for
I
being ( ( ) ( )
set
)
for
X
,
A
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) iff
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) ;
theorem
:: MBOOLEAN:19
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(Funcs)
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ,
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
c=
bool
[|
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ,
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
|]
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
begin
definition
let
I
be ( ( ) ( )
set
) ;
let
A
be ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) ;
func
union
A
->
( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
means
:: MBOOLEAN:def 2
for
i
being ( ( ) ( )
set
) st
i
: ( ( ) ( )
set
)
in
I
: ( ( ) ( )
set
) holds
it
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) )
Function-yielding
) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) )
Function-yielding
V22
() )
set
)
.
i
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
Function-like
)
set
)
=
union
(
A
: ( ( non
empty
) ( non
empty
)
set
)
.
i
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
registration
let
I
be ( ( ) ( )
set
) ;
cluster
union
(
[[0]]
I
: ( ( ) ( )
set
)
)
: ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ) (
Relation-like
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
->
Relation-like
V3
()
I
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
I
: ( ( ) ( )
set
) ) ;
end;
theorem
:: MBOOLEAN:20
for
I
being ( ( ) ( )
set
)
for
A
,
X
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
union
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) iff ex
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) &
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) ) ;
theorem
:: MBOOLEAN:21
for
I
being ( ( ) ( )
set
) holds
union
(
[[0]]
I
: ( ( ) ( )
set
)
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V3
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
[[0]]
I
: ( ( ) ( )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:22
for
I
,
x
being ( ( ) ( )
set
) holds
union
(
I
: ( ( ) ( )
set
)
-->
x
: ( ( ) ( )
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
I
: ( ( ) ( )
set
)
-->
(
union
x
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( (
Function-like
quasi_total
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
(
union
b
2
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) ;
theorem
:: MBOOLEAN:23
for
I
,
x
being ( ( ) ( )
set
) holds
union
(
I
: ( ( ) ( )
set
)
-->
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
I
: ( ( ) ( )
set
)
-->
x
: ( ( ) ( )
set
) : ( (
Function-like
quasi_total
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) ;
theorem
:: MBOOLEAN:24
for
I
,
x
,
y
being ( ( ) ( )
set
) holds
union
(
I
: ( ( ) ( )
set
)
-->
{
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
y
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
{
b
2
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
b
3
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
I
: ( ( ) ( )
set
)
-->
{
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) : ( (
Function-like
quasi_total
) (
Relation-like
non-empty
b
1
: ( ( ) ( )
set
)
-defined
Function-like
constant
V14
(
b
1
: ( ( ) ( )
set
) )
quasi_total
)
M2
(
bool
[:
b
1
: ( ( ) ( )
set
) ,
{
{
b
2
: ( ( ) ( )
set
) ,
b
3
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )) ;
theorem
:: MBOOLEAN:25
for
I
being ( ( ) ( )
set
)
for
X
,
A
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:26
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
union
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:27
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
union
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
(
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
(
union
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:28
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
union
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
(
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
(
union
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:29
for
I
being ( ( ) ( )
set
)
for
A
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
union
(
bool
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:30
for
I
being ( ( ) ( )
set
)
for
A
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) holds
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
bool
(
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:31
for
I
being ( ( ) ( )
set
)
for
Y
,
A
,
X
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
union
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) &
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:32
for
I
being ( ( ) ( )
set
)
for
Z
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
A
being ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st ( for
X
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
Z
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) holds
union
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
Z
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:33
for
I
being ( ( ) ( )
set
)
for
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
A
being ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st ( for
X
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
=
[[0]]
I
: ( ( ) ( )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ) holds
(
union
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
=
[[0]]
I
: ( ( ) ( )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:34
for
I
being ( ( ) ( )
set
)
for
A
,
B
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) is
V2
() & ( for
X
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
<>
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) &
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) &
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
=
[[0]]
I
: ( ( ) ( )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ) holds
union
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
=
(
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
(
union
B
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ;
theorem
:: MBOOLEAN:35
for
I
being ( ( ) ( )
set
)
for
A
,
X
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) )
for
B
being ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
union
(
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
\/
B
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
)
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) & ( for
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
B
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
/\
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
)
=
[[0]]
I
: ( ( ) ( )
set
) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
set
) ) holds
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
union
A
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;
theorem
:: MBOOLEAN:36
for
I
being ( ( ) ( )
set
)
for
A
being ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st ( for
X
,
Y
being ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
I
: ( ( ) ( )
set
) ) st
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) &
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) & not
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) holds
Y
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
c=
X
: ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ) holds
union
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) : ( (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) ) )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) )
in
A
: ( (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() ) (
Relation-like
V2
()
b
1
: ( ( ) ( )
set
)
-defined
Function-like
V14
(
b
1
: ( ( ) ( )
set
) )
V26
() )
ManySortedSet
of
b
1
: ( ( ) ( )
set
) ) ;