:: MEMBERED semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: 1 = succ 0
.= 0 \/ {0} by ORDINAL1:def 1
.= {0} ;

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 real-membered means :Def2: :: MEMBERED:def 2
for x being set st x in X holds
x is real;
attr X is rational-membered means :Def3: :: MEMBERED:def 3
for x being set st x in X holds
x is rational;
attr X is integer-membered means :Def4: :: MEMBERED:def 4
for x being set st x in X holds
x is integer;
attr X is natural-membered means :Def5: :: MEMBERED:def 5
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 real-membered MEMBERED:def 2 :
for X being set holds
( X is real-membered iff for x being set st x in X holds
x is real );

:: deftheorem Def3 defines rational-membered MEMBERED:def 3 :
for X being set holds
( X is rational-membered iff for x being set st x in X holds
x is rational );

:: deftheorem Def4 defines integer-membered MEMBERED:def 4 :
for X being set holds
( X is integer-membered iff for x being set st x in X holds
x is integer );

:: deftheorem Def5 defines natural-membered MEMBERED:def 5 :
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 set ;
coherence
for b1 being set st b1 is natural-membered holds
b1 is integer-membered
proof end;
cluster integer-membered -> rational-membered set ;
coherence
for b1 being set st b1 is integer-membered holds
b1 is rational-membered
proof end;
cluster rational-membered -> real-membered set ;
coherence
for b1 being set st b1 is rational-membered holds
b1 is real-membered
proof end;
cluster real-membered -> complex-membered set ;
coherence
for b1 being set st b1 is real-membered holds
b1 is complex-membered
proof end;
end;

registration
cluster non empty complex-membered real-membered rational-membered integer-membered natural-membered set ;
existence
ex b1 being set st
( not b1 is empty & b1 is natural-membered )
proof end;
end;

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

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

theorem Th1: :: MEMBERED:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is complex-membered holds
X c= COMPLEX
proof end;

theorem Th2: :: MEMBERED:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is real-membered holds
X c= REAL
proof end;

theorem Th3: :: MEMBERED:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is rational-membered holds
X c= RAT
proof end;

theorem Th4: :: MEMBERED:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is integer-membered holds
X c= INT
proof end;

theorem Th5: :: MEMBERED:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is natural-membered holds
X c= NAT
proof end;

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

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

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

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

registration
let X be natural-membered set ;
cluster -> complex natural real integer rational Element of X;
coherence
for b1 being Element of X holds b1 is natural
proof end;
end;

theorem :: MEMBERED:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty complex-membered set ex c being complex number st c in X
proof end;

theorem :: MEMBERED:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty real-membered set ex r being real number st r in X
proof end;

theorem :: MEMBERED:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty rational-membered set ex w being rational number st w in X
proof end;

theorem :: MEMBERED:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty integer-membered set ex i being integer number st i in X
proof end;

theorem :: MEMBERED:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty natural-membered set ex n being natural number st n in X
proof end;

theorem :: MEMBERED:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being complex-membered set st ( for c being complex number holds c in X ) holds
X = COMPLEX
proof end;

theorem :: MEMBERED:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being real-membered set st ( for r being real number holds r in X ) holds
X = REAL
proof end;

theorem :: MEMBERED:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being rational-membered set st ( for w being rational number holds w in X ) holds
X = RAT
proof end;

theorem :: MEMBERED:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being integer-membered set st ( for i being integer number holds i in X ) holds
X = INT
proof end;

theorem :: MEMBERED:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being natural-membered set st ( for n being natural number holds n in X ) holds
X = NAT
proof end;

theorem Th16: :: MEMBERED:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being complex-membered set st X c= Y holds
X is complex-membered
proof end;

theorem Th17: :: MEMBERED:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being real-membered set st X c= Y holds
X is real-membered
proof end;

theorem Th18: :: MEMBERED:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being rational-membered set st X c= Y holds
X is rational-membered
proof end;

theorem Th19: :: MEMBERED:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being integer-membered set st X c= Y holds
X is integer-membered
proof end;

theorem Th20: :: MEMBERED:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being natural-membered set st X c= Y holds
X is natural-membered
proof end;

registration
cluster {} -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
{} is natural-membered
proof end;
end;

registration
cluster empty -> complex-membered real-membered rational-membered integer-membered natural-membered set ;
coherence
for b1 being set st b1 is empty holds
b1 is natural-membered ;
end;

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

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

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

registration
let i be integer number ;
cluster {i} -> complex-membered real-membered rational-membered integer-membered ;
coherence
{i} is integer-membered
proof end;
end;

registration
let n be natural number ;
cluster {n} -> complex-membered real-membered rational-membered integer-membered 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 r1, r2 be real number ;
cluster {r1,r2} -> complex-membered real-membered ;
coherence
{r1,r2} is real-membered
proof end;
end;

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

registration
let i1, i2 be integer number ;
cluster {i1,i2} -> complex-membered real-membered rational-membered integer-membered ;
coherence
{i1,i2} is integer-membered
proof end;
end;

registration
let n1, n2 be natural number ;
cluster {n1,n2} -> complex-membered real-membered rational-membered integer-membered 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 r1, r2, r3 be real number ;
cluster {r1,r2,r3} -> complex-membered real-membered ;
coherence
{r1,r2,r3} is real-membered
proof end;
end;

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

registration
let i1, i2, i3 be integer number ;
cluster {i1,i2,i3} -> complex-membered real-membered rational-membered integer-membered ;
coherence
{i1,i2,i3} is integer-membered
proof end;
end;

registration
let n1, n2, n3 be natural number ;
cluster {n1,n2,n3} -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
{n1,n2,n3} is natural-membered
proof end;
end;

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

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

registration
let X be rational-membered set ;
cluster -> complex-membered real-membered rational-membered Element of K47(X);
coherence
for b1 being Subset of X holds b1 is rational-membered
proof end;
end;

registration
let X be integer-membered set ;
cluster -> complex-membered real-membered rational-membered integer-membered Element of K47(X);
coherence
for b1 being Subset of X holds b1 is integer-membered
proof end;
end;

registration
let X be natural-membered set ;
cluster -> complex-membered real-membered rational-membered integer-membered natural-membered Element of K47(X);
coherence
for b1 being Subset of X holds b1 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 real-membered set ;
cluster X \/ Y -> complex-membered real-membered ;
coherence
X \/ Y is real-membered
proof end;
end;

registration
let X, Y be rational-membered set ;
cluster X \/ Y -> complex-membered real-membered rational-membered ;
coherence
X \/ Y is rational-membered
proof end;
end;

registration
let X, Y be integer-membered set ;
cluster X \/ Y -> complex-membered real-membered rational-membered integer-membered ;
coherence
X \/ Y is integer-membered
proof end;
end;

registration
let X, Y be natural-membered set ;
cluster X \/ Y -> complex-membered real-membered rational-membered integer-membered 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
proof end;
cluster Y /\ X -> complex-membered ;
coherence
Y /\ X is complex-membered ;
end;

registration
let X be real-membered set ;
let Y be set ;
cluster X /\ Y -> complex-membered real-membered ;
coherence
X /\ Y is real-membered
proof end;
cluster Y /\ X -> complex-membered real-membered ;
coherence
Y /\ X is real-membered ;
end;

registration
let X be rational-membered set ;
let Y be set ;
cluster X /\ Y -> complex-membered real-membered rational-membered ;
coherence
X /\ Y is rational-membered
proof end;
cluster Y /\ X -> complex-membered real-membered rational-membered ;
coherence
Y /\ X is rational-membered ;
end;

registration
let X be integer-membered set ;
let Y be set ;
cluster X /\ Y -> complex-membered real-membered rational-membered integer-membered ;
coherence
X /\ Y is integer-membered
proof end;
cluster Y /\ X -> complex-membered real-membered rational-membered integer-membered ;
coherence
Y /\ X is integer-membered ;
end;

registration
let X be natural-membered set ;
let Y be set ;
cluster X /\ Y -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
X /\ Y is natural-membered
proof end;
cluster Y /\ X -> complex-membered real-membered rational-membered integer-membered 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
proof end;
end;

registration
let X be real-membered set ;
let Y be set ;
cluster X \ Y -> complex-membered real-membered ;
coherence
X \ Y is real-membered
proof end;
end;

registration
let X be rational-membered set ;
let Y be set ;
cluster X \ Y -> complex-membered real-membered rational-membered ;
coherence
X \ Y is rational-membered
proof end;
end;

registration
let X be integer-membered set ;
let Y be set ;
cluster X \ Y -> complex-membered real-membered rational-membered integer-membered ;
coherence
X \ Y is integer-membered
proof end;
end;

registration
let X be natural-membered set ;
let Y be set ;
cluster X \ Y -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
X \ Y 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 ;
end;

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

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

registration
let X, Y be integer-membered set ;
cluster X \+\ Y -> complex-membered real-membered rational-membered integer-membered ;
coherence
X \+\ Y is integer-membered ;
end;

registration
let X, Y be natural-membered set ;
cluster X \+\ Y -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
X \+\ Y is natural-membered ;
end;

definition
let X, Y be complex-membered set ;
redefine pred X c= Y means :Def6: :: MEMBERED:def 6
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 Def6 defines c= MEMBERED:def 6 :
for X, Y being complex-membered set holds
( X c= Y iff for c being complex number st c in X holds
c in Y );

definition
let X, Y be real-membered set ;
redefine pred X c= Y means :Def7: :: MEMBERED:def 7
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 Def7 defines c= MEMBERED:def 7 :
for X, Y being real-membered set holds
( X c= Y iff for r being real number st r in X holds
r in Y );

definition
let X, Y be rational-membered set ;
redefine pred X c= Y means :Def8: :: MEMBERED:def 8
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 Def8 defines c= MEMBERED:def 8 :
for X, Y being rational-membered set holds
( X c= Y iff for w being rational number st w in X holds
w in Y );

definition
let X, Y be integer-membered set ;
redefine pred X c= Y means :Def9: :: MEMBERED:def 9
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 Def9 defines c= MEMBERED:def 9 :
for X, Y being integer-membered set holds
( X c= Y iff for i being integer number st i in X holds
i in Y );

definition
let X, Y be natural-membered set ;
redefine pred X c= Y means :Def10: :: MEMBERED:def 10
for n being natural number st n in X holds
n in Y;
compatibility
( X c= Y iff for n being natural number st n in X holds
n in Y )
proof end;
end;

:: deftheorem Def10 defines c= MEMBERED:def 10 :
for X, Y being natural-membered set holds
( X c= Y iff for n being natural number st n in X holds
n in Y );

definition
let X, Y be complex-membered set ;
redefine pred X = Y means :: MEMBERED:def 11
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 11 :
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 real-membered set ;
redefine pred X = Y means :: MEMBERED:def 12
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 12 :
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 13
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 13 :
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 14
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 14 :
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 15
for n being natural number holds
( n in X iff n in Y );
compatibility
( X = Y iff for n being natural number holds
( n in X iff n in Y ) )
proof end;
end;

:: deftheorem defines = MEMBERED:def 15 :
for X, Y being natural-membered set holds
( X = Y iff for n being natural number holds
( n in X iff n in Y ) );

definition
let X, Y be complex-membered set ;
redefine pred X misses Y means :: MEMBERED:def 16
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 16 :
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 real-membered set ;
redefine pred X misses Y means :: MEMBERED:def 17
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 17 :
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 18
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 18 :
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 19
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 19 :
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 20
for n being natural number holds
( not n in X or not n in Y );
compatibility
( not X meets Y iff for n being natural number holds
( not n in X or not n in Y ) )
proof end;
end;

:: deftheorem defines meets MEMBERED:def 20 :
for X, Y being natural-membered set holds
( not X meets Y iff for n being natural number holds
( not n in X or not n in Y ) );

theorem :: MEMBERED:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, X being set st X in F & X is complex-membered holds
meet F is complex-membered
proof end;

theorem :: MEMBERED:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, X being set st X in F & X is real-membered holds
meet F is real-membered
proof end;

theorem :: MEMBERED:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, X being set st X in F & X is rational-membered holds
meet F is rational-membered
proof end;

theorem :: MEMBERED:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, X being set st X in F & X is integer-membered holds
meet F is integer-membered
proof end;

theorem :: MEMBERED:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, X being set st X in F & X is natural-membered holds
meet F is natural-membered
proof end;

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] )
proof end;

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

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

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

scheme :: MEMBERED:sch 5
NMSeparation{ P1[ set ] } :
ex X being natural-membered set st
for n being natural number holds
( n in X iff P1[n] )
proof end;