:: On the Sets Inhabited by Numbers
:: by Andrzej Trybulec
::
:: Received August 23, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
begin
definition
let
X
be
set
;
attr
X
is
complex-membered
means
:
Def1
:
:: MEMBERED:def 1
for
x
being
set
st
x
in
X
holds
x
is
complex
;
attr
X
is
ext-real-membered
means
:
Def2
:
:: MEMBERED:def 2
for
x
being
set
st
x
in
X
holds
x
is
ext-real
;
attr
X
is
real-membered
means
:
Def3
:
:: MEMBERED:def 3
for
x
being
set
st
x
in
X
holds
x
is
real
;
attr
X
is
rational-membered
means
:
Def4
:
:: MEMBERED:def 4
for
x
being
set
st
x
in
X
holds
x
is
rational
;
attr
X
is
integer-membered
means
:
Def5
:
:: MEMBERED:def 5
for
x
being
set
st
x
in
X
holds
x
is
integer
;
attr
X
is
natural-membered
means
:
Def6
:
:: MEMBERED:def 6
for
x
being
set
st
x
in
X
holds
x
is
natural
;
end;
::
deftheorem
Def1
defines
complex-membered
MEMBERED:def 1 :
for
X
being
set
holds
(
X
is
complex-membered
iff for
x
being
set
st
x
in
X
holds
x
is
complex
);
::
deftheorem
Def2
defines
ext-real-membered
MEMBERED:def 2 :
for
X
being
set
holds
(
X
is
ext-real-membered
iff for
x
being
set
st
x
in
X
holds
x
is
ext-real
);
::
deftheorem
Def3
defines
real-membered
MEMBERED:def 3 :
for
X
being
set
holds
(
X
is
real-membered
iff for
x
being
set
st
x
in
X
holds
x
is
real
);
::
deftheorem
Def4
defines
rational-membered
MEMBERED:def 4 :
for
X
being
set
holds
(
X
is
rational-membered
iff for
x
being
set
st
x
in
X
holds
x
is
rational
);
::
deftheorem
Def5
defines
integer-membered
MEMBERED:def 5 :
for
X
being
set
holds
(
X
is
integer-membered
iff for
x
being
set
st
x
in
X
holds
x
is
integer
);
::
deftheorem
Def6
defines
natural-membered
MEMBERED:def 6 :
for
X
being
set
holds
(
X
is
natural-membered
iff for
x
being
set
st
x
in
X
holds
x
is
natural
);
registration
cluster
natural-membered
->
integer-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
natural-membered
holds
b
1
is
integer-membered
proof
end;
cluster
integer-membered
->
rational-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
integer-membered
holds
b
1
is
rational-membered
proof
end;
cluster
rational-membered
->
real-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
rational-membered
holds
b
1
is
real-membered
proof
end;
cluster
real-membered
->
ext-real-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
real-membered
holds
b
1
is
ext-real-membered
proof
end;
cluster
real-membered
->
complex-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
real-membered
holds
b
1
is
complex-membered
proof
end;
end;
registration
cluster
non
empty
natural-membered
for
set
;
existence
ex
b
1
being
set
st
( not
b
1
is
empty
&
b
1
is
natural-membered
)
proof
end;
end;
registration
cluster
->
complex-membered
for
Element
of
K18
(
COMPLEX
);
coherence
for
b
1
being
Subset
of
COMPLEX
holds
b
1
is
complex-membered
proof
end;
cluster
->
ext-real-membered
for
Element
of
K18
(
ExtREAL
);
coherence
for
b
1
being
Subset
of
ExtREAL
holds
b
1
is
ext-real-membered
proof
end;
cluster
->
real-membered
for
Element
of
K18
(
REAL
);
coherence
for
b
1
being
Subset
of
REAL
holds
b
1
is
real-membered
proof
end;
cluster
->
rational-membered
for
Element
of
K18
(
RAT
);
coherence
for
b
1
being
Subset
of
RAT
holds
b
1
is
rational-membered
proof
end;
cluster
->
integer-membered
for
Element
of
K18
(
INT
);
coherence
for
b
1
being
Subset
of
INT
holds
b
1
is
integer-membered
proof
end;
cluster
->
natural-membered
for
Element
of
K18
(
NAT
);
coherence
for
b
1
being
Subset
of
NAT
holds
b
1
is
natural-membered
proof
end;
end;
registration
cluster
COMPLEX
->
complex-membered
;
coherence
COMPLEX
is
complex-membered
proof
end;
cluster
ExtREAL
->
ext-real-membered
;
coherence
ExtREAL
is
ext-real-membered
proof
end;
cluster
REAL
->
real-membered
;
coherence
REAL
is
real-membered
proof
end;
cluster
RAT
->
rational-membered
;
coherence
RAT
is
rational-membered
proof
end;
cluster
INT
->
integer-membered
;
coherence
INT
is
integer-membered
proof
end;
cluster
NAT
->
natural-membered
;
coherence
NAT
is
natural-membered
proof
end;
end;
theorem
Th1
:
:: MEMBERED:1
for
X
being
set
st
X
is
complex-membered
holds
X
c=
COMPLEX
proof
end;
theorem
Th2
:
:: MEMBERED:2
for
X
being
set
st
X
is
ext-real-membered
holds
X
c=
ExtREAL
proof
end;
theorem
Th3
:
:: MEMBERED:3
for
X
being
set
st
X
is
real-membered
holds
X
c=
REAL
proof
end;
theorem
Th4
:
:: MEMBERED:4
for
X
being
set
st
X
is
rational-membered
holds
X
c=
RAT
proof
end;
theorem
Th5
:
:: MEMBERED:5
for
X
being
set
st
X
is
integer-membered
holds
X
c=
INT
proof
end;
theorem
Th6
:
:: MEMBERED:6
for
X
being
set
st
X
is
natural-membered
holds
X
c=
NAT
proof
end;
registration
let
X
be
complex-membered
set
;
cluster
->
complex
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
complex
proof
end;
end;
registration
let
X
be
ext-real-membered
set
;
cluster
->
ext-real
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
ext-real
proof
end;
end;
registration
let
X
be
real-membered
set
;
cluster
->
real
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
real
proof
end;
end;
registration
let
X
be
rational-membered
set
;
cluster
->
rational
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
rational
proof
end;
end;
registration
let
X
be
integer-membered
set
;
cluster
->
integer
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
integer
proof
end;
end;
registration
let
X
be
natural-membered
set
;
cluster
->
natural
for
Element
of
X
;
coherence
for
b
1
being
Element
of
X
holds
b
1
is
natural
proof
end;
end;
theorem
:: MEMBERED:7
for
X
being non
empty
complex-membered
set
ex
c
being
complex
number
st
c
in
X
proof
end;
theorem
:: MEMBERED:8
for
X
being non
empty
ext-real-membered
set
ex
e
being
ext-real
number
st
e
in
X
proof
end;
theorem
:: MEMBERED:9
for
X
being non
empty
real-membered
set
ex
r
being
real
number
st
r
in
X
proof
end;
theorem
:: MEMBERED:10
for
X
being non
empty
rational-membered
set
ex
w
being
rational
number
st
w
in
X
proof
end;
theorem
:: MEMBERED:11
for
X
being non
empty
integer-membered
set
ex
i
being
integer
number
st
i
in
X
proof
end;
theorem
:: MEMBERED:12
for
X
being non
empty
natural-membered
set
ex
n
being
Nat
st
n
in
X
proof
end;
theorem
:: MEMBERED:13
for
X
being
complex-membered
set
st ( for
c
being
complex
number
holds
c
in
X
) holds
X
=
COMPLEX
proof
end;
theorem
:: MEMBERED:14
for
X
being
ext-real-membered
set
st ( for
e
being
ext-real
number
holds
e
in
X
) holds
X
=
ExtREAL
proof
end;
theorem
:: MEMBERED:15
for
X
being
real-membered
set
st ( for
r
being
real
number
holds
r
in
X
) holds
X
=
REAL
proof
end;
theorem
:: MEMBERED:16
for
X
being
rational-membered
set
st ( for
w
being
rational
number
holds
w
in
X
) holds
X
=
RAT
proof
end;
theorem
:: MEMBERED:17
for
X
being
integer-membered
set
st ( for
i
being
integer
number
holds
i
in
X
) holds
X
=
INT
proof
end;
theorem
:: MEMBERED:18
for
X
being
natural-membered
set
st ( for
n
being
Nat
holds
n
in
X
) holds
X
=
NAT
proof
end;
theorem
Th19
:
:: MEMBERED:19
for
X
being
set
for
Y
being
complex-membered
set
st
X
c=
Y
holds
X
is
complex-membered
proof
end;
theorem
Th20
:
:: MEMBERED:20
for
X
being
set
for
Y
being
ext-real-membered
set
st
X
c=
Y
holds
X
is
ext-real-membered
proof
end;
theorem
Th21
:
:: MEMBERED:21
for
X
being
set
for
Y
being
real-membered
set
st
X
c=
Y
holds
X
is
real-membered
proof
end;
theorem
Th22
:
:: MEMBERED:22
for
X
being
set
for
Y
being
rational-membered
set
st
X
c=
Y
holds
X
is
rational-membered
proof
end;
theorem
Th23
:
:: MEMBERED:23
for
X
being
set
for
Y
being
integer-membered
set
st
X
c=
Y
holds
X
is
integer-membered
proof
end;
theorem
Th24
:
:: MEMBERED:24
for
X
being
set
for
Y
being
natural-membered
set
st
X
c=
Y
holds
X
is
natural-membered
proof
end;
registration
cluster
empty
->
natural-membered
for
set
;
coherence
for
b
1
being
set
st
b
1
is
empty
holds
b
1
is
natural-membered
proof
end;
end;
registration
let
c
be
complex
number
;
cluster
{
c
}
->
complex-membered
;
coherence
{
c
}
is
complex-membered
proof
end;
end;
registration
let
e
be
ext-real
number
;
cluster
{
e
}
->
ext-real-membered
;
coherence
{
e
}
is
ext-real-membered
proof
end;
end;
registration
let
r
be
real
number
;
cluster
{
r
}
->
real-membered
;
coherence
{
r
}
is
real-membered
proof
end;
end;
registration
let
w
be
rational
number
;
cluster
{
w
}
->
rational-membered
;
coherence
{
w
}
is
rational-membered
proof
end;
end;
registration
let
i
be
integer
number
;
cluster
{
i
}
->
integer-membered
;
coherence
{
i
}
is
integer-membered
proof
end;
end;
registration
let
n
be
Nat
;
cluster
{
n
}
->
natural-membered
;
coherence
{
n
}
is
natural-membered
proof
end;
end;
registration
let
c1
,
c2
be
complex
number
;
cluster
{
c1
,
c2
}
->
complex-membered
;
coherence
{
c1
,
c2
}
is
complex-membered
proof
end;
end;
registration
let
e1
,
e2
be
ext-real
number
;
cluster
{
e1
,
e2
}
->
ext-real-membered
;
coherence
{
e1
,
e2
}
is
ext-real-membered
proof
end;
end;
registration
let
r1
,
r2
be
real
number
;
cluster
{
r1
,
r2
}
->
real-membered
;
coherence
{
r1
,
r2
}
is
real-membered
proof
end;
end;
registration
let
w1
,
w2
be
rational
number
;
cluster
{
w1
,
w2
}
->
rational-membered
;
coherence
{
w1
,
w2
}
is
rational-membered
proof
end;
end;
registration
let
i1
,
i2
be
integer
number
;
cluster
{
i1
,
i2
}
->
integer-membered
;
coherence
{
i1
,
i2
}
is
integer-membered
proof
end;
end;
registration
let
n1
,
n2
be
Nat
;
cluster
{
n1
,
n2
}
->
natural-membered
;
coherence
{
n1
,
n2
}
is
natural-membered
proof
end;
end;
registration
let
c1
,
c2
,
c3
be
complex
number
;
cluster
{
c1
,
c2
,
c3
}
->
complex-membered
;
coherence
{
c1
,
c2
,
c3
}
is
complex-membered
proof
end;
end;
registration
let
e1
,
e2
,
e3
be
ext-real
number
;
cluster
{
e1
,
e2
,
e3
}
->
ext-real-membered
;
coherence
{
e1
,
e2
,
e3
}
is
ext-real-membered
proof
end;
end;
registration
let
r1
,
r2
,
r3
be
real
number
;
cluster
{
r1
,
r2
,
r3
}
->
real-membered
;
coherence
{
r1
,
r2
,
r3
}
is
real-membered
proof
end;
end;
registration
let
w1
,
w2
,
w3
be
rational
number
;
cluster
{
w1
,
w2
,
w3
}
->
rational-membered
;
coherence
{
w1
,
w2
,
w3
}
is
rational-membered
proof
end;
end;
registration
let
i1
,
i2
,
i3
be
integer
number
;
cluster
{
i1
,
i2
,
i3
}
->
integer-membered
;
coherence
{
i1
,
i2
,
i3
}
is
integer-membered
proof
end;
end;
registration
let
n1
,
n2
,
n3
be
Nat
;
cluster
{
n1
,
n2
,
n3
}
->
natural-membered
;
coherence
{
n1
,
n2
,
n3
}
is
natural-membered
proof
end;
end;
registration
let
X
be
complex-membered
set
;
cluster
->
complex-membered
for
Element
of
K18
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
complex-membered
proof
end;
end;
registration
let
X
be
ext-real-membered
set
;
cluster
->
ext-real-membered
for
Element
of
K18
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
ext-real-membered
proof
end;
end;
registration
let
X
be
real-membered
set
;
cluster
->
real-membered
for
Element
of
K18
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
real-membered
proof
end;
end;
registration
let
X
be
rational-membered
set
;
cluster
->
rational-membered
for
Element
of
K18
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
rational-membered
proof
end;
end;
registration
let
X
be
integer-membered
set
;
cluster
->
integer-membered
for
Element
of
K18
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
integer-membered
proof
end;
end;
registration
let
X
be
natural-membered
set
;
cluster
->
natural-membered
for
Element
of
K18
(
X
);
coherence
for
b
1
being
Subset
of
X
holds
b
1
is
natural-membered
proof
end;
end;
registration
let
X
,
Y
be
complex-membered
set
;
cluster
X
\/
Y
->
complex-membered
;
coherence
X
\/
Y
is
complex-membered
proof
end;
end;
registration
let
X
,
Y
be
ext-real-membered
set
;
cluster
X
\/
Y
->
ext-real-membered
;
coherence
X
\/
Y
is
ext-real-membered
proof
end;
end;
registration
let
X
,
Y
be
real-membered
set
;
cluster
X
\/
Y
->
real-membered
;
coherence
X
\/
Y
is
real-membered
proof
end;
end;
registration
let
X
,
Y
be
rational-membered
set
;
cluster
X
\/
Y
->
rational-membered
;
coherence
X
\/
Y
is
rational-membered
proof
end;
end;
registration
let
X
,
Y
be
integer-membered
set
;
cluster
X
\/
Y
->
integer-membered
;
coherence
X
\/
Y
is
integer-membered
proof
end;
end;
registration
let
X
,
Y
be
natural-membered
set
;
cluster
X
\/
Y
->
natural-membered
;
coherence
X
\/
Y
is
natural-membered
proof
end;
end;
registration
let
X
be
complex-membered
set
;
let
Y
be
set
;
cluster
X
/\
Y
->
complex-membered
;
coherence
X
/\
Y
is
complex-membered
by
Th19
,
XBOOLE_1:17
;
cluster
Y
/\
X
->
complex-membered
;
coherence
Y
/\
X
is
complex-membered
;
end;
registration
let
X
be
ext-real-membered
set
;
let
Y
be
set
;
cluster
X
/\
Y
->
ext-real-membered
;
coherence
X
/\
Y
is
ext-real-membered
by
Th20
,
XBOOLE_1:17
;
cluster
Y
/\
X
->
ext-real-membered
;
coherence
Y
/\
X
is
ext-real-membered
;
end;
registration
let
X
be
real-membered
set
;
let
Y
be
set
;
cluster
X
/\
Y
->
real-membered
;
coherence
X
/\
Y
is
real-membered
by
Th21
,
XBOOLE_1:17
;
cluster
Y
/\
X
->
real-membered
;
coherence
Y
/\
X
is
real-membered
;
end;
registration
let
X
be
rational-membered
set
;
let
Y
be
set
;
cluster
X
/\
Y
->
rational-membered
;
coherence
X
/\
Y
is
rational-membered
by
Th22
,
XBOOLE_1:17
;
cluster
Y
/\
X
->
rational-membered
;
coherence
Y
/\
X
is
rational-membered
;
end;
registration
let
X
be
integer-membered
set
;
let
Y
be
set
;
cluster
X
/\
Y
->
integer-membered
;
coherence
X
/\
Y
is
integer-membered
by
Th23
,
XBOOLE_1:17
;
cluster
Y
/\
X
->
integer-membered
;
coherence
Y
/\
X
is
integer-membered
;
end;
registration
let
X
be
natural-membered
set
;
let
Y
be
set
;
cluster
X
/\
Y
->
natural-membered
;
coherence
X
/\
Y
is
natural-membered
by
Th24
,
XBOOLE_1:17
;
cluster
Y
/\
X
->
natural-membered
;
coherence
Y
/\
X
is
natural-membered
;
end;
registration
let
X
be
complex-membered
set
;
let
Y
be
set
;
cluster
X
\
Y
->
complex-membered
;
coherence
X
\
Y
is
complex-membered
;
end;
registration
let
X
be
ext-real-membered
set
;
let
Y
be
set
;
cluster
X
\
Y
->
ext-real-membered
;
coherence
X
\
Y
is
ext-real-membered
;
end;
registration
let
X
be
real-membered
set
;
let
Y
be
set
;
cluster
X
\
Y
->
real-membered
;
coherence
X
\
Y
is
real-membered
;
end;
registration
let
X
be
rational-membered
set
;
let
Y
be
set
;
cluster
X
\
Y
->
rational-membered
;
coherence
X
\
Y
is
rational-membered
;
end;
registration
let
X
be
integer-membered
set
;
let
Y
be
set
;
cluster
X
\
Y
->
integer-membered
;
coherence
X
\
Y
is
integer-membered
;
end;
registration
let
X
be
natural-membered
set
;
let
Y
be
set
;
cluster
X
\
Y
->
natural-membered
;
coherence
X
\
Y
is
natural-membered
;
end;
registration
let
X
,
Y
be
complex-membered
set
;
cluster
X
\+\
Y
->
complex-membered
;
coherence
X
\+\
Y
is
complex-membered
;
end;
registration
let
X
,
Y
be
ext-real-membered
set
;
cluster
X
\+\
Y
->
ext-real-membered
;
coherence
X
\+\
Y
is
ext-real-membered
;
end;
registration
let
X
,
Y
be
real-membered
set
;
cluster
X
\+\
Y
->
real-membered
;
coherence
X
\+\
Y
is
real-membered
;
end;
registration
let
X
,
Y
be
rational-membered
set
;
cluster
X
\+\
Y
->
rational-membered
;
coherence
X
\+\
Y
is
rational-membered
;
end;
registration
let
X
,
Y
be
integer-membered
set
;
cluster
X
\+\
Y
->
integer-membered
;
coherence
X
\+\
Y
is
integer-membered
;
end;
registration
let
X
,
Y
be
natural-membered
set
;
cluster
X
\+\
Y
->
natural-membered
;
coherence
X
\+\
Y
is
natural-membered
;
end;
definition
let
X
be
complex-membered
set
;
let
Y
be
set
;
redefine
pred
X
c=
Y
means
:
Def7
:
:: MEMBERED:def 7
for
c
being
complex
number
st
c
in
X
holds
c
in
Y
;
compatibility
(
X
c=
Y
iff for
c
being
complex
number
st
c
in
X
holds
c
in
Y
)
proof
end;
end;
::
deftheorem
Def7
defines
c=
MEMBERED:def 7 :
for
X
being
complex-membered
set
for
Y
being
set
holds
(
X
c=
Y
iff for
c
being
complex
number
st
c
in
X
holds
c
in
Y
);
definition
let
X
be
ext-real-membered
set
;
let
Y
be
set
;
redefine
pred
X
c=
Y
means
:
Def8
:
:: MEMBERED:def 8
for
e
being
ext-real
number
st
e
in
X
holds
e
in
Y
;
compatibility
(
X
c=
Y
iff for
e
being
ext-real
number
st
e
in
X
holds
e
in
Y
)
proof
end;
end;
::
deftheorem
Def8
defines
c=
MEMBERED:def 8 :
for
X
being
ext-real-membered
set
for
Y
being
set
holds
(
X
c=
Y
iff for
e
being
ext-real
number
st
e
in
X
holds
e
in
Y
);
definition
let
X
be
real-membered
set
;
let
Y
be
set
;
redefine
pred
X
c=
Y
means
:
Def9
:
:: MEMBERED:def 9
for
r
being
real
number
st
r
in
X
holds
r
in
Y
;
compatibility
(
X
c=
Y
iff for
r
being
real
number
st
r
in
X
holds
r
in
Y
)
proof
end;
end;
::
deftheorem
Def9
defines
c=
MEMBERED:def 9 :
for
X
being
real-membered
set
for
Y
being
set
holds
(
X
c=
Y
iff for
r
being
real
number
st
r
in
X
holds
r
in
Y
);
definition
let
X
be
rational-membered
set
;
let
Y
be
set
;
redefine
pred
X
c=
Y
means
:
Def10
:
:: MEMBERED:def 10
for
w
being
rational
number
st
w
in
X
holds
w
in
Y
;
compatibility
(
X
c=
Y
iff for
w
being
rational
number
st
w
in
X
holds
w
in
Y
)
proof
end;
end;
::
deftheorem
Def10
defines
c=
MEMBERED:def 10 :
for
X
being
rational-membered
set
for
Y
being
set
holds
(
X
c=
Y
iff for
w
being
rational
number
st
w
in
X
holds
w
in
Y
);
definition
let
X
be
integer-membered
set
;
let
Y
be
set
;
redefine
pred
X
c=
Y
means
:
Def11
:
:: MEMBERED:def 11
for
i
being
integer
number
st
i
in
X
holds
i
in
Y
;
compatibility
(
X
c=
Y
iff for
i
being
integer
number
st
i
in
X
holds
i
in
Y
)
proof
end;
end;
::
deftheorem
Def11
defines
c=
MEMBERED:def 11 :
for
X
being
integer-membered
set
for
Y
being
set
holds
(
X
c=
Y
iff for
i
being
integer
number
st
i
in
X
holds
i
in
Y
);
definition
let
X
be
natural-membered
set
;
let
Y
be
set
;
redefine
pred
X
c=
Y
means
:
Def12
:
:: MEMBERED:def 12
for
n
being
Nat
st
n
in
X
holds
n
in
Y
;
compatibility
(
X
c=
Y
iff for
n
being
Nat
st
n
in
X
holds
n
in
Y
)
proof
end;
end;
::
deftheorem
Def12
defines
c=
MEMBERED:def 12 :
for
X
being
natural-membered
set
for
Y
being
set
holds
(
X
c=
Y
iff for
n
being
Nat
st
n
in
X
holds
n
in
Y
);
definition
let
X
,
Y
be
complex-membered
set
;
redefine
pred
X
=
Y
means
:: MEMBERED:def 13
for
c
being
complex
number
holds
(
c
in
X
iff
c
in
Y
);
compatibility
(
X
=
Y
iff for
c
being
complex
number
holds
(
c
in
X
iff
c
in
Y
) )
proof
end;
end;
::
deftheorem
defines
=
MEMBERED:def 13 :
for
X
,
Y
being
complex-membered
set
holds
(
X
=
Y
iff for
c
being
complex
number
holds
(
c
in
X
iff
c
in
Y
) );
definition
let
X
,
Y
be
ext-real-membered
set
;
redefine
pred
X
=
Y
means
:: MEMBERED:def 14
for
e
being
ext-real
number
holds
(
e
in
X
iff
e
in
Y
);
compatibility
(
X
=
Y
iff for
e
being
ext-real
number
holds
(
e
in
X
iff
e
in
Y
) )
proof
end;
end;
::
deftheorem
defines
=
MEMBERED:def 14 :
for
X
,
Y
being
ext-real-membered
set
holds
(
X
=
Y
iff for
e
being
ext-real
number
holds
(
e
in
X
iff
e
in
Y
) );
definition
let
X
,
Y
be
real-membered
set
;
redefine
pred
X
=
Y
means
:: MEMBERED:def 15
for
r
being
real
number
holds
(
r
in
X
iff
r
in
Y
);
compatibility
(
X
=
Y
iff for
r
being
real
number
holds
(
r
in
X
iff
r
in
Y
) )
proof
end;
end;
::
deftheorem
defines
=
MEMBERED:def 15 :
for
X
,
Y
being
real-membered
set
holds
(
X
=
Y
iff for
r
being
real
number
holds
(
r
in
X
iff
r
in
Y
) );
definition
let
X
,
Y
be
rational-membered
set
;
redefine
pred
X
=
Y
means
:: MEMBERED:def 16
for
w
being
rational
number
holds
(
w
in
X
iff
w
in
Y
);
compatibility
(
X
=
Y
iff for
w
being
rational
number
holds
(
w
in
X
iff
w
in
Y
) )
proof
end;
end;
::
deftheorem
defines
=
MEMBERED:def 16 :
for
X
,
Y
being
rational-membered
set
holds
(
X
=
Y
iff for
w
being
rational
number
holds
(
w
in
X
iff
w
in
Y
) );
definition
let
X
,
Y
be
integer-membered
set
;
redefine
pred
X
=
Y
means
:: MEMBERED:def 17
for
i
being
integer
number
holds
(
i
in
X
iff
i
in
Y
);
compatibility
(
X
=
Y
iff for
i
being
integer
number
holds
(
i
in
X
iff
i
in
Y
) )
proof
end;
end;
::
deftheorem
defines
=
MEMBERED:def 17 :
for
X
,
Y
being
integer-membered
set
holds
(
X
=
Y
iff for
i
being
integer
number
holds
(
i
in
X
iff
i
in
Y
) );
definition
let
X
,
Y
be
natural-membered
set
;
redefine
pred
X
=
Y
means
:: MEMBERED:def 18
for
n
being
Nat
holds
(
n
in
X
iff
n
in
Y
);
compatibility
(
X
=
Y
iff for
n
being
Nat
holds
(
n
in
X
iff
n
in
Y
) )
proof
end;
end;
::
deftheorem
defines
=
MEMBERED:def 18 :
for
X
,
Y
being
natural-membered
set
holds
(
X
=
Y
iff for
n
being
Nat
holds
(
n
in
X
iff
n
in
Y
) );
definition
let
X
,
Y
be
complex-membered
set
;
redefine
pred
X
misses
Y
means
:: MEMBERED:def 19
for
c
being
complex
number
holds
( not
c
in
X
or not
c
in
Y
);
compatibility
( not
X
meets
Y
iff for
c
being
complex
number
holds
( not
c
in
X
or not
c
in
Y
) )
proof
end;
end;
::
deftheorem
defines
meets
MEMBERED:def 19 :
for
X
,
Y
being
complex-membered
set
holds
( not
X
meets
Y
iff for
c
being
complex
number
holds
( not
c
in
X
or not
c
in
Y
) );
definition
let
X
,
Y
be
ext-real-membered
set
;
redefine
pred
X
misses
Y
means
:: MEMBERED:def 20
for
e
being
ext-real
number
holds
( not
e
in
X
or not
e
in
Y
);
compatibility
( not
X
meets
Y
iff for
e
being
ext-real
number
holds
( not
e
in
X
or not
e
in
Y
) )
proof
end;
end;
::
deftheorem
defines
meets
MEMBERED:def 20 :
for
X
,
Y
being
ext-real-membered
set
holds
( not
X
meets
Y
iff for
e
being
ext-real
number
holds
( not
e
in
X
or not
e
in
Y
) );
definition
let
X
,
Y
be
real-membered
set
;
redefine
pred
X
misses
Y
means
:: MEMBERED:def 21
for
r
being
real
number
holds
( not
r
in
X
or not
r
in
Y
);
compatibility
( not
X
meets
Y
iff for
r
being
real
number
holds
( not
r
in
X
or not
r
in
Y
) )
proof
end;
end;
::
deftheorem
defines
meets
MEMBERED:def 21 :
for
X
,
Y
being
real-membered
set
holds
( not
X
meets
Y
iff for
r
being
real
number
holds
( not
r
in
X
or not
r
in
Y
) );
definition
let
X
,
Y
be
rational-membered
set
;
redefine
pred
X
misses
Y
means
:: MEMBERED:def 22
for
w
being
rational
number
holds
( not
w
in
X
or not
w
in
Y
);
compatibility
( not
X
meets
Y
iff for
w
being
rational
number
holds
( not
w
in
X
or not
w
in
Y
) )
proof
end;
end;
::
deftheorem
defines
meets
MEMBERED:def 22 :
for
X
,
Y
being
rational-membered
set
holds
( not
X
meets
Y
iff for
w
being
rational
number
holds
( not
w
in
X
or not
w
in
Y
) );
definition
let
X
,
Y
be
integer-membered
set
;
redefine
pred
X
misses
Y
means
:: MEMBERED:def 23
for
i
being
integer
number
holds
( not
i
in
X
or not
i
in
Y
);
compatibility
( not
X
meets
Y
iff for
i
being
integer
number
holds
( not
i
in
X
or not
i
in
Y
) )
proof
end;
end;
::
deftheorem
defines
meets
MEMBERED:def 23 :
for
X
,
Y
being
integer-membered
set
holds
( not
X
meets
Y
iff for
i
being
integer
number
holds
( not
i
in
X
or not
i
in
Y
) );
definition
let
X
,
Y
be
natural-membered
set
;
redefine
pred
X
misses
Y
means
:: MEMBERED:def 24
for
n
being
Nat
holds
( not
n
in
X
or not
n
in
Y
);
compatibility
( not
X
meets
Y
iff for
n
being
Nat
holds
( not
n
in
X
or not
n
in
Y
) )
proof
end;
end;
::
deftheorem
defines
meets
MEMBERED:def 24 :
for
X
,
Y
being
natural-membered
set
holds
( not
X
meets
Y
iff for
n
being
Nat
holds
( not
n
in
X
or not
n
in
Y
) );
theorem
:: MEMBERED:25
for
F
being
set
st ( for
X
being
set
st
X
in
F
holds
X
is
complex-membered
) holds
union
F
is
complex-membered
proof
end;
theorem
:: MEMBERED:26
for
F
being
set
st ( for
X
being
set
st
X
in
F
holds
X
is
ext-real-membered
) holds
union
F
is
ext-real-membered
proof
end;
theorem
:: MEMBERED:27
for
F
being
set
st ( for
X
being
set
st
X
in
F
holds
X
is
real-membered
) holds
union
F
is
real-membered
proof
end;
theorem
:: MEMBERED:28
for
F
being
set
st ( for
X
being
set
st
X
in
F
holds
X
is
rational-membered
) holds
union
F
is
rational-membered
proof
end;
theorem
:: MEMBERED:29
for
F
being
set
st ( for
X
being
set
st
X
in
F
holds
X
is
integer-membered
) holds
union
F
is
integer-membered
proof
end;
theorem
:: MEMBERED:30
for
F
being
set
st ( for
X
being
set
st
X
in
F
holds
X
is
natural-membered
) holds
union
F
is
natural-membered
proof
end;
theorem
:: MEMBERED:31
for
F
,
X
being
set
st
X
in
F
&
X
is
complex-membered
holds
meet
F
is
complex-membered
by
Th19
,
SETFAM_1:3
;
theorem
:: MEMBERED:32
for
F
,
X
being
set
st
X
in
F
&
X
is
ext-real-membered
holds
meet
F
is
ext-real-membered
by
Th20
,
SETFAM_1:3
;
theorem
:: MEMBERED:33
for
F
,
X
being
set
st
X
in
F
&
X
is
real-membered
holds
meet
F
is
real-membered
by
Th21
,
SETFAM_1:3
;
theorem
:: MEMBERED:34
for
F
,
X
being
set
st
X
in
F
&
X
is
rational-membered
holds
meet
F
is
rational-membered
by
Th22
,
SETFAM_1:3
;
theorem
:: MEMBERED:35
for
F
,
X
being
set
st
X
in
F
&
X
is
integer-membered
holds
meet
F
is
integer-membered
by
Th23
,
SETFAM_1:3
;
theorem
:: MEMBERED:36
for
F
,
X
being
set
st
X
in
F
&
X
is
natural-membered
holds
meet
F
is
natural-membered
by
Th24
,
SETFAM_1:3
;
scheme
:: MEMBERED:sch 1
CMSeparation
{
P
1
[
set
] } :
ex
X
being
complex-membered
set
st
for
c
being
complex
number
holds
(
c
in
X
iff
P
1
[
c
] )
proof
end;
scheme
:: MEMBERED:sch 2
EMSeparation
{
P
1
[
set
] } :
ex
X
being
ext-real-membered
set
st
for
e
being
ext-real
number
holds
(
e
in
X
iff
P
1
[
e
] )
proof
end;
scheme
:: MEMBERED:sch 3
RMSeparation
{
P
1
[
set
] } :
ex
X
being
real-membered
set
st
for
r
being
real
number
holds
(
r
in
X
iff
P
1
[
r
] )
proof
end;
scheme
:: MEMBERED:sch 4
WMSeparation
{
P
1
[
set
] } :
ex
X
being
rational-membered
set
st
for
w
being
rational
number
holds
(
w
in
X
iff
P
1
[
w
] )
proof
end;
scheme
:: MEMBERED:sch 5
IMSeparation
{
P
1
[
set
] } :
ex
X
being
integer-membered
set
st
for
i
being
integer
number
holds
(
i
in
X
iff
P
1
[
i
] )
proof
end;
scheme
:: MEMBERED:sch 6
NMSeparation
{
P
1
[
set
] } :
ex
X
being
natural-membered
set
st
for
n
being
Nat
holds
(
n
in
X
iff
P
1
[
n
] )
proof
end;
registration
cluster
non
empty
natural-membered
for
set
;
existence
ex
b
1
being
set
st
( not
b
1
is
empty
&
b
1
is
natural-membered
)
proof
end;
end;
:: Added by AK, 2008.02.02
registration
cluster
->
natural-membered
for
Element
of
NAT
;
coherence
for
b
1
being
Element
of
NAT
holds
b
1
is
natural-membered
proof
end;
end;
theorem
:: MEMBERED:37
for
X
,
Y
being
real-membered
set
st
X
<>
{}
&
Y
<>
{}
& ( for
a
,
b
being
real
number
st
a
in
X
&
b
in
Y
holds
a
<=
b
) holds
ex
d
being
real
number
st
( ( for
a
being
real
number
st
a
in
X
holds
a
<=
d
) & ( for
b
being
real
number
st
b
in
Y
holds
d
<=
b
) )
proof
end;
:: Added, AK, 2010.04.23
definition
let
X
be
set
;
attr
X
is
add-closed
means
:: MEMBERED:def 25
for
x
,
y
being
complex
number
st
x
in
X
&
y
in
X
holds
x
+
y
in
X
;
end;
::
deftheorem
defines
add-closed
MEMBERED:def 25 :
for
X
being
set
holds
(
X
is
add-closed
iff for
x
,
y
being
complex
number
st
x
in
X
&
y
in
X
holds
x
+
y
in
X
);
registration
cluster
empty
->
add-closed
for
set
;
coherence
for
b
1
being
set
st
b
1
is
empty
holds
b
1
is
add-closed
proof
end;
cluster
COMPLEX
->
add-closed
;
coherence
COMPLEX
is
add-closed
proof
end;
cluster
REAL
->
add-closed
;
coherence
REAL
is
add-closed
proof
end;
cluster
RAT
->
add-closed
;
coherence
RAT
is
add-closed
proof
end;
cluster
INT
->
add-closed
;
coherence
INT
is
add-closed
proof
end;
cluster
NAT
->
add-closed
;
coherence
NAT
is
add-closed
proof
end;
cluster
non
empty
natural-membered
add-closed
for
set
;
existence
ex
b
1
being
set
st
( not
b
1
is
empty
&
b
1
is
add-closed
&
b
1
is
natural-membered
)
proof
end;
end;