:: REALSET1 semantic presentation
begin
theorem
:: REALSET1:1
for
X
,
x
being ( ( ) ( )
set
)
for
F
being ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
Function
of
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
set
)
in
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) holds
F
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
Function
of
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) )
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
X
: ( ( ) ( )
set
) ;
definition
let
X
be ( ( ) ( )
set
) ;
let
F
be ( (
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) )
BinOp
of
X
: ( ( ) ( )
set
) ) ;
mode
Preserv
of
F
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
V36
()
V40
() )
set
) )
means
:: REALSET1:def 1
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
[:
it
: ( ( ) ( )
set
) ,
it
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) holds
F
: ( ( ) ( )
set
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
it
: ( ( ) ( )
set
) ;
end;
definition
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
let
A
be ( ( ) ( )
set
) ;
func
R
||
A
->
( ( ) ( )
set
)
equals
:: REALSET1:def 2
R
: ( (
V35
() ) (
V31
()
V35
()
V36
()
cardinal
)
set
)
|
[:
A
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) ;
end;
registration
let
R
be ( (
Relation-like
) (
Relation-like
)
Relation
) ;
let
A
be ( ( ) ( )
set
) ;
cluster
R
: ( (
Relation-like
) (
Relation-like
)
set
)
||
A
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
->
Relation-like
;
end;
registration
let
R
be ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
let
A
be ( ( ) ( )
set
) ;
cluster
R
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
||
A
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
)
set
)
->
Function-like
;
end;
theorem
:: REALSET1:2
for
X
being ( ( ) ( )
set
)
for
F
being ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
X
: ( ( ) ( )
set
) )
for
A
being ( ( ) ( )
Preserv
of
F
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) holds
F
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) )
||
A
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) : ( ( ) (
Relation-like
Function-like
)
set
) is ( (
Function-like
V18
(
[:
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) ,
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) )
:]
: ( ( ) ( )
set
) ,
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) ) ) (
Relation-like
[:
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) ,
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) )
:]
: ( ( ) ( )
set
)
-defined
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) )
-valued
Function-like
V18
(
[:
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) ,
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) )
:]
: ( ( ) ( )
set
) ,
b
3
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) ) )
BinOp
of
A
: ( ( ) ( )
Preserv
of
b
2
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) ) ) ) ;
definition
let
X
be ( ( ) ( )
set
) ;
let
F
be ( (
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) )
BinOp
of
X
: ( ( ) ( )
set
) ) ;
let
A
be ( ( ) ( )
Preserv
of
F
: ( (
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) )
BinOp
of
X
: ( ( ) ( )
set
) ) ) ;
:: original:
||
redefine
func
F
||
A
->
( (
Function-like
V18
(
[:
A
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
A
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
A
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
A
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
set
) ) )
BinOp
of
A
: ( ( ) ( )
set
) ) ;
end;
theorem
:: REALSET1:3
for
X
being ( ( ) ( )
set
) holds
( not
X
: ( ( ) ( )
set
) is
trivial
iff for
x
being ( ( ) ( )
set
) holds
X
: ( ( ) ( )
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) : ( ( ) ( )
Element
of
bool
b
1
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
) ( non
empty
)
set
) ) ;
theorem
:: REALSET1:4
ex
A
being ( ( non
empty
) ( non
empty
)
set
) st
for
z
being ( ( ) ( )
Element
of
A
: ( ( non
empty
) ( non
empty
)
set
) ) holds
A
: ( ( non
empty
) ( non
empty
)
set
)
\
{
z
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
) ( non
empty
)
set
) ;
definition
let
X
be ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ;
let
F
be ( (
Function-like
V18
(
[:
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ) (
Relation-like
[:
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
-valued
Function-like
V18
(
[:
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) )
BinOp
of
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ;
let
x
be ( ( ) ( )
Element
of
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ;
pred
F
is_Bin_Op_Preserv
x
means
:: REALSET1:def 3
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Preserv
of
F
: ( ( non
empty
) ( non
empty
)
set
) ) &
(
F
: ( ( non
empty
) ( non
empty
)
set
)
||
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
)
: ( ( ) ( )
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
(
F
: ( ( non
empty
) ( non
empty
)
set
)
||
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is ( (
Function-like
V18
(
[:
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) (
Relation-like
[:
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
)
-defined
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V18
(
[:
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
BinOp
of
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) );
end;
theorem
:: REALSET1:5
for
X
being ( ( ) ( )
set
)
for
A
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ex
F
being ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
X
: ( ( ) ( )
set
) ) st
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
[:
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) holds
F
: ( (
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
BinOp
of
b
1
: ( ( ) ( )
set
) )
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
definition
let
X
be ( ( ) ( )
set
) ;
let
A
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
mode
Presv
of
X
,
A
->
( (
Function-like
V18
(
[:
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ) (
Relation-like
[:
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
-valued
Function-like
V18
(
[:
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) )
BinOp
of
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
means
:: REALSET1:def 4
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) holds
it
: ( ( ) ( )
set
)
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
A
: ( ( non
empty
) ( non
empty
)
set
) ;
end;
theorem
:: REALSET1:6
for
X
being ( ( ) ( )
set
)
for
A
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
F
being ( ( ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
Presv
of
X
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) holds
F
: ( ( ) (
Relation-like
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( ) ( )
set
) ) )
Presv
of
b
1
: ( ( ) ( )
set
) ,
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) )
||
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
Relation-like
Function-like
)
set
) is ( (
Function-like
V18
(
[:
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ) (
Relation-like
[:
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
)
-defined
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V18
(
[:
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ,
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
b
2
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) )
BinOp
of
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
X
be ( ( ) ( )
set
) ;
let
A
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
let
F
be ( ( ) (
Relation-like
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
Function-like
V18
(
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) ) )
Presv
of
X
: ( ( ) ( )
set
) ,
A
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;
func
F
|||
A
->
( (
Function-like
V18
(
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
) ) ) (
Relation-like
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
A
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V18
(
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
) ) )
BinOp
of
A
: ( ( non
empty
) ( non
empty
)
set
) )
equals
:: REALSET1:def 5
F
: ( ( ) ( )
set
)
||
A
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ;
end;
definition
let
A
be ( ( ) ( )
set
) ;
let
x
be ( ( ) ( )
Element
of
A
: ( ( ) ( )
set
) ) ;
mode
DnT
of
x
,
A
->
( (
Function-like
V18
(
[:
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ) (
Relation-like
[:
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
-valued
Function-like
V18
(
[:
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) )
BinOp
of
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
means
:: REALSET1:def 6
for
y
being ( ( ) ( )
set
) st
y
: ( ( ) ( )
set
)
in
[:
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) holds
it
: ( ( ) ( )
set
)
.
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) : ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: REALSET1:7
for
A
being ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
for
x
being ( ( ) ( )
Element
of
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
for
F
being ( ( ) (
Relation-like
[:
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) )
DnT
of
x
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) holds
F
: ( ( ) (
Relation-like
[:
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
-valued
Function-like
V18
(
[:
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) )
DnT
of
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
||
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
Relation-like
Function-like
)
set
) is ( (
Function-like
V18
(
[:
(
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) (
Relation-like
[:
(
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
)
-defined
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V18
(
[:
(
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
b
2
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
BinOp
of
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
definition
let
A
be ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ;
let
x
be ( ( ) ( )
Element
of
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ;
let
F
be ( ( ) (
Relation-like
[:
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
-valued
Function-like
V18
(
[:
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) )
DnT
of
x
: ( ( ) ( )
Element
of
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) ;
func
F
!
(
A
,
x
)
->
( (
Function-like
V18
(
[:
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) (
Relation-like
[:
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
)
-defined
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
-valued
Function-like
V18
(
[:
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
:]
: ( ( ) ( )
set
) ,
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
BinOp
of
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) )
equals
:: REALSET1:def 7
F
: ( ( ) ( )
set
)
||
(
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
{
x
: ( ( non
empty
) ( non
empty
)
set
)
}
: ( ( ) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
A
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ;
end;
theorem
:: REALSET1:8
for
F
being ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
for
A
being ( ( 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Singleton
of ( ( ) ( non
empty
)
set
) ) holds
F
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
A
: ( ( 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Singleton
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
) ( non
empty
)
set
) ;
registration
let
F
be ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ;
let
A
be ( ( 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Singleton
of ( ( ) ( non
empty
)
set
) ) ;
cluster
F
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
\
A
: ( ( 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
) ( non
empty
trivial
V36
() 1 : ( ( ) ( non
empty
V26
()
V27
()
V31
()
V35
()
V36
()
cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
() )
Element
of
K168
() : ( ( ) ( non
empty
non
trivial
V31
()
V36
()
cardinal
limit_cardinal
V44
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
bool
K164
() : ( ( ) (
V44
()
V45
()
V46
()
V50
() )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
Element
of
bool
F
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
->
non
empty
;
end;