:: On the Sets Inhabited by Numbers
:: by Andrzej Trybulec
::
:: Received August 23, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

definition

let X be set ;

attr X is complex-membered means :Def1: :: MEMBERED:def 1
for x being object st x in X holds
x is complex ;

attr X is ext-real-membered means :Def2: :: MEMBERED:def 2
for x being object st x in X holds
x is ext-real ;

attr X is real-membered means :Def3: :: MEMBERED:def 3
for x being object st x in X holds
x is real ;

attr X is rational-membered means :Def4: :: MEMBERED:def 4
for x being object st x in X holds
x is rational ;

attr X is integer-membered means :Def5: :: MEMBERED:def 5
for x being object st x in X holds
x is integer ;

attr X is natural-membered means :Def6: :: MEMBERED:def 6
for x being object 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 object 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 object 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 object 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 object 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 object 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 object st x in X holds
x is natural );

registration

cluster natural-membered -> integer-membered for set ;

coherence
for b₁ being set st b₁ is natural-membered holds
b₁ is integer-membered

proof end;

cluster integer-membered -> rational-membered for set ;

coherence
for b₁ being set st b₁ is integer-membered holds
b₁ is rational-membered

proof end;

cluster rational-membered -> real-membered for set ;

coherence
for b₁ being set st b₁ is rational-membered holds
b₁ is real-membered

proof end;

cluster real-membered -> ext-real-membered for set ;

coherence
for b₁ being set st b₁ is real-membered holds
b₁ is ext-real-membered

proof end;

cluster real-membered -> complex-membered for set ;

coherence
for b₁ being set st b₁ is real-membered holds
b₁ is complex-membered

proof end;

end;

registration

cluster non empty natural-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is natural-membered )

proof end;

end;

registration

cluster COMPLEX -> complex-membered ;

coherence
COMPLEX is complex-membered ;

cluster ExtREAL -> ext-real-membered ;

coherence
ExtREAL is ext-real-membered

proof end;

cluster REAL -> real-membered ;

coherence
REAL is real-membered ;

cluster RAT -> rational-membered ;

coherence
RAT is rational-membered

proof end;

cluster INT -> integer-membered ;

coherence
INT is integer-membered ;

cluster omega -> natural-membered ;

coherence
NAT is natural-membered ;

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 by ORDINAL1:def 12;

registration

let X be complex-membered set ;

cluster -> complex for Element of X;

coherence
for b₁ being Element of X holds b₁ is complex

proof end;

end;

registration

let X be ext-real-membered set ;

cluster -> ext-real for Element of X;

coherence
for b₁ being Element of X holds b₁ is ext-real

proof end;

end;

registration

let X be real-membered set ;

cluster -> real for Element of X;

coherence
for b₁ being Element of X holds b₁ is real

proof end;

end;

registration

let X be rational-membered set ;

cluster -> rational for Element of X;

coherence
for b₁ being Element of X holds b₁ is rational

proof end;

end;

registration

let X be integer-membered set ;

cluster -> integer for Element of X;

coherence
for b₁ being Element of X holds b₁ is integer

proof end;

end;

registration

let X be natural-membered set ;

cluster -> natural for Element of X;

coherence
for b₁ being Element of X holds b₁ is natural

proof end;

end;

theorem :: MEMBERED:7

for X being non empty complex-membered set ex c being Complex st c in X

proof end;

theorem :: MEMBERED:8

for X being non empty ext-real-membered set ex e being ExtReal st e in X

proof end;

theorem :: MEMBERED:9

for X being non empty real-membered set ex r being Real st r in X

proof end;

theorem :: MEMBERED:10

for X being non empty rational-membered set ex w being Rational st w in X

proof end;

theorem :: MEMBERED:11

for X being non empty integer-membered set ex i being Integer 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 holds c in X ) holds
X = COMPLEX

proof end;

theorem :: MEMBERED:14

for X being ext-real-membered set st ( for e being ExtReal holds e in X ) holds
X = ExtREAL

proof end;

theorem :: MEMBERED:15

for X being real-membered set st ( for r being Real holds r in X ) holds
X = REAL

proof end;

theorem :: MEMBERED:16

for X being rational-membered set st ( for w being Rational holds w in X ) holds
X = RAT

proof end;

theorem :: MEMBERED:17

for X being integer-membered set st ( for i being Integer 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 ;

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 ;

theorem Th21: :: MEMBERED:21

for X being set
for Y being real-membered set st X c= Y holds
X is real-membered ;

theorem Th22: :: MEMBERED:22

for X being set
for Y being rational-membered set st X c= Y holds
X is rational-membered ;

theorem Th23: :: MEMBERED:23

for X being set
for Y being integer-membered set st X c= Y holds
X is integer-membered ;

theorem Th24: :: MEMBERED:24

for X being set
for Y being natural-membered set st X c= Y holds
X is natural-membered ;

registration

cluster empty -> natural-membered for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is natural-membered ;

end;

registration

let c be Complex;

cluster {c} -> complex-membered ;

coherence
{c} is complex-membered by TARSKI:def 1;

end;

registration

let e be ExtReal;

cluster {e} -> ext-real-membered ;

coherence
{e} is ext-real-membered by TARSKI:def 1;

end;

registration

let r be Real;

cluster {r} -> real-membered ;

coherence
{r} is real-membered by TARSKI:def 1;

end;

registration

let w be Rational;

cluster {w} -> rational-membered ;

coherence
{w} is rational-membered by TARSKI:def 1;

end;

registration

let i be Integer;

cluster {i} -> integer-membered ;

coherence
{i} is integer-membered by TARSKI:def 1;

end;

registration

let n be Nat;

cluster {n} -> natural-membered ;

coherence
{n} is natural-membered by TARSKI:def 1;

end;

registration

let c1, c2 be Complex;

cluster {c1,c2} -> complex-membered ;

coherence
{c1,c2} is complex-membered by TARSKI:def 2;

end;

registration

let e1, e2 be ExtReal;

cluster {e1,e2} -> ext-real-membered ;

coherence
{e1,e2} is ext-real-membered by TARSKI:def 2;

end;

registration

let r1, r2 be Real;

cluster {r1,r2} -> real-membered ;

coherence
{r1,r2} is real-membered by TARSKI:def 2;

end;

registration

let w1, w2 be Rational;

cluster {w1,w2} -> rational-membered ;

coherence
{w1,w2} is rational-membered by TARSKI:def 2;

end;

registration

let i1, i2 be Integer;

cluster {i1,i2} -> integer-membered ;

coherence
{i1,i2} is integer-membered by TARSKI:def 2;

end;

registration

let n1, n2 be Nat;

cluster {n1,n2} -> natural-membered ;

coherence
{n1,n2} is natural-membered by TARSKI:def 2;

end;

registration

let c1, c2, c3 be Complex;

cluster {c1,c2,c3} -> complex-membered ;

coherence
{c1,c2,c3} is complex-membered by ENUMSET1:def 1;

end;

registration

let e1, e2, e3 be ExtReal;

cluster {e1,e2,e3} -> ext-real-membered ;

coherence
{e1,e2,e3} is ext-real-membered by ENUMSET1:def 1;

end;

registration

let r1, r2, r3 be Real;

cluster {r1,r2,r3} -> real-membered ;

coherence
{r1,r2,r3} is real-membered by ENUMSET1:def 1;

end;

registration

let w1, w2, w3 be Rational;

cluster {w1,w2,w3} -> rational-membered ;

coherence
{w1,w2,w3} is rational-membered by ENUMSET1:def 1;

end;

registration

let i1, i2, i3 be Integer;

cluster {i1,i2,i3} -> integer-membered ;

coherence
{i1,i2,i3} is integer-membered by ENUMSET1:def 1;

end;

registration

let n1, n2, n3 be Nat;

cluster {n1,n2,n3} -> natural-membered ;

coherence
{n1,n2,n3} is natural-membered by ENUMSET1:def 1;

end;

registration

let X be complex-membered set ;

cluster -> complex-membered for Element of K18(X);

coherence
for b₁ being Subset of X holds b₁ is complex-membered ;

end;

registration

let X be ext-real-membered set ;

cluster -> ext-real-membered for Element of K18(X);

coherence
for b₁ being Subset of X holds b₁ is ext-real-membered ;

end;

registration

let X be real-membered set ;

cluster -> real-membered for Element of K18(X);

coherence
for b₁ being Subset of X holds b₁ is real-membered ;

end;

registration

let X be rational-membered set ;

cluster -> rational-membered for Element of K18(X);

coherence
for b₁ being Subset of X holds b₁ is rational-membered ;

end;

registration

let X be integer-membered set ;

cluster -> integer-membered for Element of K18(X);

coherence
for b₁ being Subset of X holds b₁ is integer-membered ;

end;

registration

let X be natural-membered set ;

cluster -> natural-membered for Element of K18(X);

coherence
for b₁ being Subset of X holds b₁ is natural-membered ;

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 :: MEMBERED:def 7
for c being Complex st c in X holds
c in Y;

compatibility
( X c= Y iff for c being Complex st c in X holds
c in Y ) ;

end;

:: deftheorem defines c= MEMBERED:def 7 :
for X being complex-membered set
for Y being set holds
( X c= Y iff for c being Complex 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 :: MEMBERED:def 8
for e being ExtReal st e in X holds
e in Y;

compatibility
( X c= Y iff for e being ExtReal st e in X holds
e in Y ) ;

end;

:: deftheorem defines c= MEMBERED:def 8 :
for X being ext-real-membered set
for Y being set holds
( X c= Y iff for e being ExtReal 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 :: MEMBERED:def 9
for r being Real st r in X holds
r in Y;

compatibility
( X c= Y iff for r being Real st r in X holds
r in Y ) ;

end;

:: deftheorem defines c= MEMBERED:def 9 :
for X being real-membered set
for Y being set holds
( X c= Y iff for r being Real 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 :: MEMBERED:def 10
for w being Rational st w in X holds
w in Y;

compatibility
( X c= Y iff for w being Rational st w in X holds
w in Y ) ;

end;

:: deftheorem defines c= MEMBERED:def 10 :
for X being rational-membered set
for Y being set holds
( X c= Y iff for w being Rational 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 :: MEMBERED:def 11
for i being Integer st i in X holds
i in Y;

compatibility
( X c= Y iff for i being Integer st i in X holds
i in Y ) ;

end;

:: deftheorem defines c= MEMBERED:def 11 :
for X being integer-membered set
for Y being set holds
( X c= Y iff for i being Integer 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 :: 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 ) ;

end;

:: deftheorem 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 holds
( c in X iff c in Y );

compatibility
( X = Y iff for c being Complex 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 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 ExtReal holds
( e in X iff e in Y );

compatibility
( X = Y iff for e being ExtReal 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 ExtReal 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 holds
( r in X iff r in Y );

compatibility
( X = Y iff for r being Real holds
( r in X iff r in Y ) ) ;

end;

:: deftheorem defines = MEMBERED:def 15 :
for X, Y being real-membered set holds
( X = Y iff for r being Real 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 holds
( w in X iff w in Y );

compatibility
( X = Y iff for w being Rational holds
( w in X iff w in Y ) ) ;

end;

:: deftheorem defines = MEMBERED:def 16 :
for X, Y being rational-membered set holds
( X = Y iff for w being Rational 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 holds
( i in X iff i in Y );

compatibility
( X = Y iff for i being Integer holds
( i in X iff i in Y ) ) ;

end;

:: deftheorem defines = MEMBERED:def 17 :
for X, Y being integer-membered set holds
( X = Y iff for i being Integer 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 ) ) ;

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 holds
( not c in X or not c in Y );

compatibility
( X misses Y iff for c being Complex holds
( not c in X or not c in Y ) )

proof end;

end;

:: deftheorem defines misses MEMBERED:def 19 :
for X, Y being complex-membered set holds
( X misses Y iff for c being Complex 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 ExtReal holds
( not e in X or not e in Y );

compatibility
( X misses Y iff for e being ExtReal holds
( not e in X or not e in Y ) )

proof end;

end;

:: deftheorem defines misses MEMBERED:def 20 :
for X, Y being ext-real-membered set holds
( X misses Y iff for e being ExtReal 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 holds
( not r in X or not r in Y );

compatibility
( X misses Y iff for r being Real holds
( not r in X or not r in Y ) ) ;

end;

:: deftheorem defines misses MEMBERED:def 21 :
for X, Y being real-membered set holds
( X misses Y iff for r being Real 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 holds
( not w in X or not w in Y );

compatibility
( X misses Y iff for w being Rational holds
( not w in X or not w in Y ) ) ;

end;

:: deftheorem defines misses MEMBERED:def 22 :
for X, Y being rational-membered set holds
( X misses Y iff for w being Rational 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 holds
( not i in X or not i in Y );

compatibility
( X misses Y iff for i being Integer holds
( not i in X or not i in Y ) ) ;

end;

:: deftheorem defines misses MEMBERED:def 23 :
for X, Y being integer-membered set holds
( X misses Y iff for i being Integer 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
( X misses Y iff for n being Nat holds
( not n in X or not n in Y ) ) ;

end;

:: deftheorem defines misses MEMBERED:def 24 :
for X, Y being natural-membered set holds
( X misses 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₁[ object ] } :

ex X being complex-membered set st
for c being Complex holds
( c in X iff P₁[c] )

proof end;

scheme :: MEMBERED:sch 2
EMSeparation{ P₁[ object ] } :

ex X being ext-real-membered set st
for e being ExtReal holds
( e in X iff P₁[e] )

proof end;

scheme :: MEMBERED:sch 3
RMSeparation{ P₁[ object ] } :

ex X being real-membered set st
for r being Real holds
( r in X iff P₁[r] )

proof end;

scheme :: MEMBERED:sch 4
WMSeparation{ P₁[ object ] } :

ex X being rational-membered set st
for w being Rational holds
( w in X iff P₁[w] )

proof end;

scheme :: MEMBERED:sch 5
IMSeparation{ P₁[ object ] } :

ex X being integer-membered set st
for i being Integer holds
( i in X iff P₁[i] )

proof end;

scheme :: MEMBERED:sch 6
NMSeparation{ P₁[ object ] } :

ex X being natural-membered set st
for n being Nat holds
( n in X iff P₁[n] )

proof end;

registration

cluster non empty natural-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is natural-membered )

proof end;

end;

theorem :: MEMBERED:37

for X, Y being real-membered set st X <> {} & Y <> {} & ( for a, b being Real st a in X & b in Y holds
a <= b ) holds
ex d being Real st
( ( for a being Real st a in X holds
a <= d ) & ( for b being Real 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 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 st x in X & y in X holds
x + y in X );

registration

cluster empty -> add-closed for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is add-closed ;

cluster COMPLEX -> add-closed ;

coherence
COMPLEX is add-closed by XCMPLX_0:def 2;

cluster REAL -> add-closed ;

coherence
REAL is add-closed by XREAL_0:def 1;

cluster RAT -> add-closed ;

coherence
RAT is add-closed by RAT_1:def 2;

cluster INT -> add-closed ;

coherence
INT is add-closed by INT_1:def 2;

cluster omega -> add-closed ;

coherence
NAT is add-closed by ORDINAL1:def 12;

cluster non empty natural-membered add-closed for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is add-closed & b₁ is natural-membered )

proof end;

end;