:: 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 ;
attrX is complex-membered  means :Def1: :: MEMBERED:def 1
 for x being set st x in X holds
x is complex ;
attrX is ext-real-membered  means :Def2: :: MEMBERED:def 2
 for x being set st x in X holds
x is ext-real ;
attrX is real-membered  means :Def3: :: MEMBERED:def 3
 for x being set st x in X holds
x is real ;
attrX is rational-membered  means :Def4: :: MEMBERED:def 4
 for x being set st x in X holds
x is rational ;
attrX is integer-membered  means :Def5: :: MEMBERED:def 5
 for x being set st x in X holds
x is integer ;
attrX 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 b1 being set st b1 is natural-membered holds
b1 is integer-membered
proofend;
cluster integer-membered  ->  rational-membered for set ;
coherence
 for b1 being set st b1 is integer-membered holds
b1 is rational-membered
proofend;
cluster rational-membered  ->  real-membered for set ;
coherence
 for b1 being set st b1 is rational-membered holds
b1 is real-membered
proofend;
cluster real-membered  ->  ext-real-membered for set ;
coherence
 for b1 being set st b1 is real-membered holds
b1 is ext-real-membered
proofend;
cluster real-membered  ->  complex-membered for set ;
coherence
 for b1 being set st b1 is real-membered holds
b1 is complex-membered
proofend;
end;

registration
cluster non empty natural-membered for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is natural-membered )
proofend;
end;

registration
cluster  ->  complex-membered for Element of K18(COMPLEX);
coherence
 for b1 being Subset of COMPLEX holds b1 is complex-membered
proofend;
cluster  ->  ext-real-membered for Element of K18(ExtREAL);
coherence
 for b1 being Subset of ExtREAL holds b1 is ext-real-membered
proofend;
cluster  ->  real-membered for Element of K18(REAL);
coherence
 for b1 being Subset of REAL holds b1 is real-membered
proofend;
cluster  ->  rational-membered for Element of K18(RAT);
coherence
 for b1 being Subset of RAT holds b1 is rational-membered
proofend;
cluster  ->  integer-membered for Element of K18(INT);
coherence
 for b1 being Subset of INT holds b1 is integer-membered
proofend;
cluster  ->  natural-membered for Element of K18(NAT);
coherence
 for b1 being Subset of NAT holds b1 is natural-membered
proofend;
end;

registration
cluster COMPLEX  ->  complex-membered ;
coherence
 COMPLEX is complex-membered
proofend;
cluster ExtREAL  ->  ext-real-membered ;
coherence
 ExtREAL is ext-real-membered
proofend;
cluster REAL  ->  real-membered ;
coherence
 REAL is real-membered
proofend;
cluster RAT  ->  rational-membered ;
coherence
 RAT is rational-membered
proofend;
cluster INT  ->  integer-membered ;
coherence
 INT is integer-membered
proofend;
cluster NAT  ->  natural-membered ;
coherence
 NAT is natural-membered
proofend;
end;

theorem Th1: :: MEMBERED:1
for X being set st X is complex-membered holds
X c= COMPLEX
proofend;

theorem Th2: :: MEMBERED:2
for X being set st X is ext-real-membered holds
X c= ExtREAL
proofend;

theorem Th3: :: MEMBERED:3
for X being set st X is real-membered holds
X c= REAL
proofend;

theorem Th4: :: MEMBERED:4
for X being set st X is rational-membered holds
X c= RAT
proofend;

theorem Th5: :: MEMBERED:5
for X being set st X is integer-membered holds
X c= INT
proofend;

theorem Th6: :: MEMBERED:6
for X being set st X is natural-membered holds
X c= NAT
proofend;

registration
let X be complex-membered set ;
cluster  ->  complex for Element of X;
coherence
 for b1 being Element of X holds b1 is complex
proofend;
end;

registration
let X be ext-real-membered set ;
cluster  ->  ext-real for Element of X;
coherence
 for b1 being Element of X holds b1 is ext-real
proofend;
end;

registration
let X be real-membered set ;
cluster  ->  real for Element of X;
coherence
 for b1 being Element of X holds b1 is real
proofend;
end;

registration
let X be rational-membered set ;
cluster  ->  rational for Element of X;
coherence
 for b1 being Element of X holds b1 is rational
proofend;
end;

registration
let X be integer-membered set ;
cluster  ->  integer for Element of X;
coherence
 for b1 being Element of X holds b1 is integer
proofend;
end;

registration
let X be natural-membered set ;
cluster  ->  natural for Element of X;
coherence
 for b1 being Element of X holds b1 is natural
proofend;
end;

theorem :: MEMBERED:7
for X being non empty complex-membered set ex c being complex number st c in X
proofend;

theorem :: MEMBERED:8
for X being non empty ext-real-membered set ex e being ext-real number st e in X
proofend;

theorem :: MEMBERED:9
for X being non empty real-membered set ex r being real number st r in X
proofend;

theorem :: MEMBERED:10
for X being non empty rational-membered set ex w being rational number st w in X
proofend;

theorem :: MEMBERED:11
for X being non empty integer-membered set ex i being integer number st i in X
proofend;

theorem :: MEMBERED:12
for X being non empty natural-membered set ex n being Nat st n in X
proofend;

theorem :: MEMBERED:13
for X being complex-membered set st ( for c being complex number holds c in X ) holds
X = COMPLEX
proofend;

theorem :: MEMBERED:14
for X being ext-real-membered set st ( for e being ext-real number holds e in X ) holds
X = ExtREAL
proofend;

theorem :: MEMBERED:15
for X being real-membered set st ( for r being real number holds r in X ) holds
X = REAL
proofend;

theorem :: MEMBERED:16
for X being rational-membered set st ( for w being rational number holds w in X ) holds
X = RAT
proofend;

theorem :: MEMBERED:17
for X being integer-membered set st ( for i being integer number holds i in X ) holds
X = INT
proofend;

theorem :: MEMBERED:18
for X being natural-membered set st ( for n being Nat holds n in X ) holds
X = NAT
proofend;

theorem Th19: :: MEMBERED:19
for X being set
for Y being complex-membered set st X c= Y holds
X is complex-membered
proofend;

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
proofend;

theorem Th21: :: MEMBERED:21
for X being set
for Y being real-membered set st X c= Y holds
X is real-membered
proofend;

theorem Th22: :: MEMBERED:22
for X being set
for Y being rational-membered set st X c= Y holds
X is rational-membered
proofend;

theorem Th23: :: MEMBERED:23
for X being set
for Y being integer-membered set st X c= Y holds
X is integer-membered
proofend;

theorem Th24: :: MEMBERED:24
for X being set
for Y being natural-membered set st X c= Y holds
X is natural-membered
proofend;

registration
cluster empty  ->  natural-membered for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is natural-membered
proofend;
end;

registration
let c be complex number ;
cluster{c} ->  complex-membered ;
coherence
 {c} is complex-membered
proofend;
end;

registration
let e be ext-real number ;
cluster{e} ->  ext-real-membered ;
coherence
 {e} is ext-real-membered
proofend;
end;

registration
let r be real number ;
cluster{r} ->  real-membered ;
coherence
 {r} is real-membered
proofend;
end;

registration
let w be rational number ;
cluster{w} ->  rational-membered ;
coherence
 {w} is rational-membered
proofend;
end;

registration
let i be integer number ;
cluster{i} ->  integer-membered ;
coherence
 {i} is integer-membered
proofend;
end;

registration
let n be Nat;
cluster{n} ->  natural-membered ;
coherence
 {n} is natural-membered
proofend;
end;

registration
let c1, c2 be complex number ;
cluster{c1,c2} ->  complex-membered ;
coherence
 {c1,c2} is complex-membered
proofend;
end;

registration
let e1, e2 be ext-real number ;
cluster{e1,e2} ->  ext-real-membered ;
coherence
 {e1,e2} is ext-real-membered
proofend;
end;

registration
let r1, r2 be real number ;
cluster{r1,r2} ->  real-membered ;
coherence
 {r1,r2} is real-membered
proofend;
end;

registration
let w1, w2 be rational number ;
cluster{w1,w2} ->  rational-membered ;
coherence
 {w1,w2} is rational-membered
proofend;
end;

registration
let i1, i2 be integer number ;
cluster{i1,i2} ->  integer-membered ;
coherence
 {i1,i2} is integer-membered
proofend;
end;

registration
let n1, n2 be Nat;
cluster{n1,n2} ->  natural-membered ;
coherence
 {n1,n2} is natural-membered
proofend;
end;

registration
let c1, c2, c3 be complex number ;
cluster{c1,c2,c3} ->  complex-membered ;
coherence
 {c1,c2,c3} is complex-membered
proofend;
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
proofend;
end;

registration
let r1, r2, r3 be real number ;
cluster{r1,r2,r3} ->  real-membered ;
coherence
 {r1,r2,r3} is real-membered
proofend;
end;

registration
let w1, w2, w3 be rational number ;
cluster{w1,w2,w3} ->  rational-membered ;
coherence
 {w1,w2,w3} is rational-membered
proofend;
end;

registration
let i1, i2, i3 be integer number ;
cluster{i1,i2,i3} ->  integer-membered ;
coherence
 {i1,i2,i3} is integer-membered
proofend;
end;

registration
let n1, n2, n3 be Nat;
cluster{n1,n2,n3} ->  natural-membered ;
coherence
 {n1,n2,n3} is natural-membered
proofend;
end;

registration
let X be complex-membered set ;
cluster  ->  complex-membered for Element of K18(X);
coherence
 for b1 being Subset of X holds b1 is complex-membered
proofend;
end;

registration
let X be ext-real-membered set ;
cluster  ->  ext-real-membered for Element of K18(X);
coherence
 for b1 being Subset of X holds b1 is ext-real-membered
proofend;
end;

registration
let X be real-membered set ;
cluster  ->  real-membered for Element of K18(X);
coherence
 for b1 being Subset of X holds b1 is real-membered
proofend;
end;

registration
let X be rational-membered set ;
cluster  ->  rational-membered for Element of K18(X);
coherence
 for b1 being Subset of X holds b1 is rational-membered
proofend;
end;

registration
let X be integer-membered set ;
cluster  ->  integer-membered for Element of K18(X);
coherence
 for b1 being Subset of X holds b1 is integer-membered
proofend;
end;

registration
let X be natural-membered set ;
cluster  ->  natural-membered for Element of K18(X);
coherence
 for b1 being Subset of X holds b1 is natural-membered
proofend;
end;

registration
let X, Y be complex-membered set ;
clusterX \/ Y ->  complex-membered ;
coherence
 X \/ Y is complex-membered
proofend;
end;

registration
let X, Y be ext-real-membered set ;
clusterX \/ Y ->  ext-real-membered ;
coherence
 X \/ Y is ext-real-membered
proofend;
end;

registration
let X, Y be real-membered set ;
clusterX \/ Y ->  real-membered ;
coherence
 X \/ Y is real-membered
proofend;
end;

registration
let X, Y be rational-membered set ;
clusterX \/ Y ->  rational-membered ;
coherence
 X \/ Y is rational-membered
proofend;
end;

registration
let X, Y be integer-membered set ;
clusterX \/ Y ->  integer-membered ;
coherence
 X \/ Y is integer-membered
proofend;
end;

registration
let X, Y be natural-membered set ;
clusterX \/ Y ->  natural-membered ;
coherence
 X \/ Y is natural-membered
proofend;
end;

registration
let X be complex-membered set ;
let Y be set ;
clusterX /\ Y ->  complex-membered ;
coherence
 X /\ Y is complex-membered by Th19, XBOOLE_1:17;
clusterY /\ X ->  complex-membered ;
coherence
 Y /\ X is complex-membered ;
end;

registration
let X be ext-real-membered set ;
let Y be set ;
clusterX /\ Y ->  ext-real-membered ;
coherence
 X /\ Y is ext-real-membered by Th20, XBOOLE_1:17;
clusterY /\ X ->  ext-real-membered ;
coherence
 Y /\ X is ext-real-membered ;
end;

registration
let X be real-membered set ;
let Y be set ;
clusterX /\ Y ->  real-membered ;
coherence
 X /\ Y is real-membered by Th21, XBOOLE_1:17;
clusterY /\ X ->  real-membered ;
coherence
 Y /\ X is real-membered ;
end;

registration
let X be rational-membered set ;
let Y be set ;
clusterX /\ Y ->  rational-membered ;
coherence
 X /\ Y is rational-membered by Th22, XBOOLE_1:17;
clusterY /\ X ->  rational-membered ;
coherence
 Y /\ X is rational-membered ;
end;

registration
let X be integer-membered set ;
let Y be set ;
clusterX /\ Y ->  integer-membered ;
coherence
 X /\ Y is integer-membered by Th23, XBOOLE_1:17;
clusterY /\ X ->  integer-membered ;
coherence
 Y /\ X is integer-membered ;
end;

registration
let X be natural-membered set ;
let Y be set ;
clusterX /\ Y ->  natural-membered ;
coherence
 X /\ Y is natural-membered by Th24, XBOOLE_1:17;
clusterY /\ X ->  natural-membered ;
coherence
 Y /\ X is natural-membered ;
end;

registration
let X be complex-membered set ;
let Y be set ;
clusterX \ Y ->  complex-membered ;
coherence
 X \ Y is complex-membered ;
end;

registration
let X be ext-real-membered set ;
let Y be set ;
clusterX \ Y ->  ext-real-membered ;
coherence
 X \ Y is ext-real-membered ;
end;

registration
let X be real-membered set ;
let Y be set ;
clusterX \ Y ->  real-membered ;
coherence
 X \ Y is real-membered ;
end;

registration
let X be rational-membered set ;
let Y be set ;
clusterX \ Y ->  rational-membered ;
coherence
 X \ Y is rational-membered ;
end;

registration
let X be integer-membered set ;
let Y be set ;
clusterX \ Y ->  integer-membered ;
coherence
 X \ Y is integer-membered ;
end;

registration
let X be natural-membered set ;
let Y be set ;
clusterX \ Y ->  natural-membered ;
coherence
 X \ Y is natural-membered ;
end;

registration
let X, Y be complex-membered set ;
clusterX \+\ Y ->  complex-membered ;
coherence
 X \+\ Y is complex-membered ;
end;

registration
let X, Y be ext-real-membered set ;
clusterX \+\ Y ->  ext-real-membered ;
coherence
 X \+\ Y is ext-real-membered ;
end;

registration
let X, Y be real-membered set ;
clusterX \+\ Y ->  real-membered ;
coherence
 X \+\ Y is real-membered ;
end;

registration
let X, Y be rational-membered set ;
clusterX \+\ Y ->  rational-membered ;
coherence
 X \+\ Y is rational-membered ;
end;

registration
let X, Y be integer-membered set ;
clusterX \+\ Y ->  integer-membered ;
coherence
 X \+\ Y is integer-membered ;
end;

registration
let X, Y be natural-membered set ;
clusterX \+\ 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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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 ) )
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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{ P1[ set ] } :
 ex X being complex-membered set st
for c being complex number holds
( c in X iff P1[c] )
proofend;

scheme :: MEMBERED:sch 2
EMSeparation{ P1[ set ] } :
 ex X being ext-real-membered set st
for e being ext-real number holds
( e in X iff P1[e] )
proofend;

scheme :: MEMBERED:sch 3
RMSeparation{ P1[ set ] } :
 ex X being real-membered set st
for r being real number holds
( r in X iff P1[r] )
proofend;

scheme :: MEMBERED:sch 4
WMSeparation{ P1[ set ] } :
 ex X being rational-membered set st
for w being rational number holds
( w in X iff P1[w] )
proofend;

scheme :: MEMBERED:sch 5
IMSeparation{ P1[ set ] } :
 ex X being integer-membered set st
for i being integer number holds
( i in X iff P1[i] )
proofend;

scheme :: MEMBERED:sch 6
NMSeparation{ P1[ set ] } :
 ex X being natural-membered set st
for n being Nat holds
( n in X iff P1[n] )
proofend;

registration
cluster non empty natural-membered for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is natural-membered )
proofend;
end;

:: Added by AK, 2008.02.02
registration
cluster  ->  natural-membered for Element of NAT ;
coherence
 for b1 being Element of NAT holds b1 is natural-membered
proofend;
end;

theorem :: MEMBERED:37
for X, Y being real-membered set st X <> {} &amp; Y <> {} &amp; ( for a, b being real number st a in X &amp; 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 ) &amp; ( for b being real number st b in Y holds
d <= b ) )
proofend;

:: Added, AK, 2010.04.23
definition
let X be set ;
attrX is add-closed  means :: MEMBERED:def 25
 for x, y being complex number st x in X &amp; 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 &amp; y in X holds
x + y in X );

registration
cluster empty  ->  add-closed for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is add-closed
proofend;
cluster COMPLEX  ->  add-closed ;
coherence
 COMPLEX is add-closed
proofend;
cluster REAL  ->  add-closed ;
coherence
 REAL is add-closed
proofend;
cluster RAT  ->  add-closed ;
coherence
 RAT is add-closed
proofend;
cluster INT  ->  add-closed ;
coherence
 INT is add-closed
proofend;
cluster NAT  ->  add-closed ;
coherence
 NAT is add-closed
proofend;
cluster non empty natural-membered add-closed for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is add-closed &amp; b1 is natural-membered )
proofend;
end;