:: MEMBERED semantic presentation

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

definition
let c1 be set ;
attr a1 is complex-membered means :Def1: :: MEMBERED:def 1
for b1 being set st b1 in a1 holds
b1 is complex;
attr a1 is real-membered means :Def2: :: MEMBERED:def 2
for b1 being set st b1 in a1 holds
b1 is real;
attr a1 is rational-membered means :Def3: :: MEMBERED:def 3
for b1 being set st b1 in a1 holds
b1 is rational;
attr a1 is integer-membered means :Def4: :: MEMBERED:def 4
for b1 being set st b1 in a1 holds
b1 is integer;
attr a1 is natural-membered means :Def5: :: MEMBERED:def 5
for b1 being set st b1 in a1 holds
b1 is natural;
end;

:: deftheorem Def1 defines complex-membered MEMBERED:def 1 :
for b1 being set holds
( b1 is complex-membered iff for b2 being set st b2 in b1 holds
b2 is complex );

:: deftheorem Def2 defines real-membered MEMBERED:def 2 :
for b1 being set holds
( b1 is real-membered iff for b2 being set st b2 in b1 holds
b2 is real );

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

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

:: deftheorem Def5 defines natural-membered MEMBERED:def 5 :
for b1 being set holds
( b1 is natural-membered iff for b2 being set st b2 in b1 holds
b2 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
for b1 being set st b1 is complex-membered holds
b1 c= COMPLEX
proof end;

theorem Th2: :: MEMBERED:2
for b1 being set st b1 is real-membered holds
b1 c= REAL
proof end;

theorem Th3: :: MEMBERED:3
for b1 being set st b1 is rational-membered holds
b1 c= RAT
proof end;

theorem Th4: :: MEMBERED:4
for b1 being set st b1 is integer-membered holds
b1 c= INT
proof end;

theorem Th5: :: MEMBERED:5
for b1 being set st b1 is natural-membered holds
b1 c= NAT
proof end;

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

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

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

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

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

theorem Th6: :: MEMBERED:6
for b1 being non empty complex-membered set ex b2 being complex number st b2 in b1
proof end;

theorem Th7: :: MEMBERED:7
for b1 being non empty real-membered set ex b2 being real number st b2 in b1
proof end;

theorem Th8: :: MEMBERED:8
for b1 being non empty rational-membered set ex b2 being rational number st b2 in b1
proof end;

theorem Th9: :: MEMBERED:9
for b1 being non empty integer-membered set ex b2 being integer number st b2 in b1
proof end;

theorem Th10: :: MEMBERED:10
for b1 being non empty natural-membered set ex b2 being natural number st b2 in b1
proof end;

theorem Th11: :: MEMBERED:11
for b1 being complex-membered set st ( for b2 being complex number holds b2 in b1 ) holds
b1 = COMPLEX
proof end;

theorem Th12: :: MEMBERED:12
for b1 being real-membered set st ( for b2 being real number holds b2 in b1 ) holds
b1 = REAL
proof end;

theorem Th13: :: MEMBERED:13
for b1 being rational-membered set st ( for b2 being rational number holds b2 in b1 ) holds
b1 = RAT
proof end;

theorem Th14: :: MEMBERED:14
for b1 being integer-membered set st ( for b2 being integer number holds b2 in b1 ) holds
b1 = INT
proof end;

theorem Th15: :: MEMBERED:15
for b1 being natural-membered set st ( for b2 being natural number holds b2 in b1 ) holds
b1 = NAT
proof end;

theorem Th16: :: MEMBERED:16
for b1 being set
for b2 being complex-membered set st b1 c= b2 holds
b1 is complex-membered
proof end;

theorem Th17: :: MEMBERED:17
for b1 being set
for b2 being real-membered set st b1 c= b2 holds
b1 is real-membered
proof end;

theorem Th18: :: MEMBERED:18
for b1 being set
for b2 being rational-membered set st b1 c= b2 holds
b1 is rational-membered
proof end;

theorem Th19: :: MEMBERED:19
for b1 being set
for b2 being integer-membered set st b1 c= b2 holds
b1 is integer-membered
proof end;

theorem Th20: :: MEMBERED:20
for b1 being set
for b2 being natural-membered set st b1 c= b2 holds
b1 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 c1 be complex number ;
cluster {a1} -> complex-membered ;
coherence
{c1} is complex-membered
proof end;
end;

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

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

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

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

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

registration
let c1, c2 be real number ;
cluster {a1,a2} -> complex-membered real-membered ;
coherence
{c1,c2} is real-membered
proof end;
end;

registration
let c1, c2 be rational number ;
cluster {a1,a2} -> complex-membered real-membered rational-membered ;
coherence
{c1,c2} is rational-membered
proof end;
end;

registration
let c1, c2 be integer number ;
cluster {a1,a2} -> complex-membered real-membered rational-membered integer-membered ;
coherence
{c1,c2} is integer-membered
proof end;
end;

registration
let c1, c2 be natural number ;
cluster {a1,a2} -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
{c1,c2} is natural-membered
proof end;
end;

registration
let c1, c2, c3 be complex number ;
cluster {a1,a2,a3} -> complex-membered ;
coherence
{c1,c2,c3} is complex-membered
proof end;
end;

registration
let c1, c2, c3 be real number ;
cluster {a1,a2,a3} -> complex-membered real-membered ;
coherence
{c1,c2,c3} is real-membered
proof end;
end;

registration
let c1, c2, c3 be rational number ;
cluster {a1,a2,a3} -> complex-membered real-membered rational-membered ;
coherence
{c1,c2,c3} is rational-membered
proof end;
end;

registration
let c1, c2, c3 be integer number ;
cluster {a1,a2,a3} -> complex-membered real-membered rational-membered integer-membered ;
coherence
{c1,c2,c3} is integer-membered
proof end;
end;

registration
let c1, c2, c3 be natural number ;
cluster {a1,a2,a3} -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
{c1,c2,c3} is natural-membered
proof end;
end;

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

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

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

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

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

registration
let c1, c2 be complex-membered set ;
cluster a1 \/ a2 -> complex-membered ;
coherence
c1 \/ c2 is complex-membered
proof end;
end;

registration
let c1, c2 be real-membered set ;
cluster a1 \/ a2 -> complex-membered real-membered ;
coherence
c1 \/ c2 is real-membered
proof end;
end;

registration
let c1, c2 be rational-membered set ;
cluster a1 \/ a2 -> complex-membered real-membered rational-membered ;
coherence
c1 \/ c2 is rational-membered
proof end;
end;

registration
let c1, c2 be integer-membered set ;
cluster a1 \/ a2 -> complex-membered real-membered rational-membered integer-membered ;
coherence
c1 \/ c2 is integer-membered
proof end;
end;

registration
let c1, c2 be natural-membered set ;
cluster a1 \/ a2 -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
c1 \/ c2 is natural-membered
proof end;
end;

registration
let c1 be complex-membered set ;
let c2 be set ;
cluster a1 /\ a2 -> complex-membered ;
coherence
c1 /\ c2 is complex-membered
proof end;
cluster a2 /\ a1 -> complex-membered ;
coherence
c2 /\ c1 is complex-membered ;
end;

registration
let c1 be real-membered set ;
let c2 be set ;
cluster a1 /\ a2 -> complex-membered real-membered ;
coherence
c1 /\ c2 is real-membered
proof end;
cluster a2 /\ a1 -> complex-membered real-membered ;
coherence
c2 /\ c1 is real-membered ;
end;

registration
let c1 be rational-membered set ;
let c2 be set ;
cluster a1 /\ a2 -> complex-membered real-membered rational-membered ;
coherence
c1 /\ c2 is rational-membered
proof end;
cluster a2 /\ a1 -> complex-membered real-membered rational-membered ;
coherence
c2 /\ c1 is rational-membered ;
end;

registration
let c1 be integer-membered set ;
let c2 be set ;
cluster a1 /\ a2 -> complex-membered real-membered rational-membered integer-membered ;
coherence
c1 /\ c2 is integer-membered
proof end;
cluster a2 /\ a1 -> complex-membered real-membered rational-membered integer-membered ;
coherence
c2 /\ c1 is integer-membered ;
end;

registration
let c1 be natural-membered set ;
let c2 be set ;
cluster a1 /\ a2 -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
c1 /\ c2 is natural-membered
proof end;
cluster a2 /\ a1 -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
c2 /\ c1 is natural-membered ;
end;

registration
let c1 be complex-membered set ;
let c2 be set ;
cluster a1 \ a2 -> complex-membered ;
coherence
c1 \ c2 is complex-membered
proof end;
end;

registration
let c1 be real-membered set ;
let c2 be set ;
cluster a1 \ a2 -> complex-membered real-membered ;
coherence
c1 \ c2 is real-membered
proof end;
end;

registration
let c1 be rational-membered set ;
let c2 be set ;
cluster a1 \ a2 -> complex-membered real-membered rational-membered ;
coherence
c1 \ c2 is rational-membered
proof end;
end;

registration
let c1 be integer-membered set ;
let c2 be set ;
cluster a1 \ a2 -> complex-membered real-membered rational-membered integer-membered ;
coherence
c1 \ c2 is integer-membered
proof end;
end;

registration
let c1 be natural-membered set ;
let c2 be set ;
cluster a1 \ a2 -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
c1 \ c2 is natural-membered
proof end;
end;

registration
let c1, c2 be complex-membered set ;
cluster a1 \+\ a2 -> complex-membered ;
coherence
c1 \+\ c2 is complex-membered ;
end;

registration
let c1, c2 be real-membered set ;
cluster a1 \+\ a2 -> complex-membered real-membered ;
coherence
c1 \+\ c2 is real-membered ;
end;

registration
let c1, c2 be rational-membered set ;
cluster a1 \+\ a2 -> complex-membered real-membered rational-membered ;
coherence
c1 \+\ c2 is rational-membered ;
end;

registration
let c1, c2 be integer-membered set ;
cluster a1 \+\ a2 -> complex-membered real-membered rational-membered integer-membered ;
coherence
c1 \+\ c2 is integer-membered ;
end;

registration
let c1, c2 be natural-membered set ;
cluster a1 \+\ a2 -> complex-membered real-membered rational-membered integer-membered natural-membered ;
coherence
c1 \+\ c2 is natural-membered ;
end;

definition
let c1, c2 be complex-membered set ;
redefine pred c1 c= c2 means :Def6: :: MEMBERED:def 6
for b1 being complex number st b1 in a1 holds
b1 in a2;
compatibility
( c1 c= c2 iff for b1 being complex number st b1 in c1 holds
b1 in c2 )
proof end;
end;

:: deftheorem Def6 defines c= MEMBERED:def 6 :
for b1, b2 being complex-membered set holds
( b1 c= b2 iff for b3 being complex number st b3 in b1 holds
b3 in b2 );

definition
let c1, c2 be real-membered set ;
redefine pred c1 c= c2 means :Def7: :: MEMBERED:def 7
for b1 being real number st b1 in a1 holds
b1 in a2;
compatibility
( c1 c= c2 iff for b1 being real number st b1 in c1 holds
b1 in c2 )
proof end;
end;

:: deftheorem Def7 defines c= MEMBERED:def 7 :
for b1, b2 being real-membered set holds
( b1 c= b2 iff for b3 being real number st b3 in b1 holds
b3 in b2 );

definition
let c1, c2 be rational-membered set ;
redefine pred c1 c= c2 means :Def8: :: MEMBERED:def 8
for b1 being rational number st b1 in a1 holds
b1 in a2;
compatibility
( c1 c= c2 iff for b1 being rational number st b1 in c1 holds
b1 in c2 )
proof end;
end;

:: deftheorem Def8 defines c= MEMBERED:def 8 :
for b1, b2 being rational-membered set holds
( b1 c= b2 iff for b3 being rational number st b3 in b1 holds
b3 in b2 );

definition
let c1, c2 be integer-membered set ;
redefine pred c1 c= c2 means :Def9: :: MEMBERED:def 9
for b1 being integer number st b1 in a1 holds
b1 in a2;
compatibility
( c1 c= c2 iff for b1 being integer number st b1 in c1 holds
b1 in c2 )
proof end;
end;

:: deftheorem Def9 defines c= MEMBERED:def 9 :
for b1, b2 being integer-membered set holds
( b1 c= b2 iff for b3 being integer number st b3 in b1 holds
b3 in b2 );

definition
let c1, c2 be natural-membered set ;
redefine pred c1 c= c2 means :Def10: :: MEMBERED:def 10
for b1 being natural number st b1 in a1 holds
b1 in a2;
compatibility
( c1 c= c2 iff for b1 being natural number st b1 in c1 holds
b1 in c2 )
proof end;
end;

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

definition
let c1, c2 be complex-membered set ;
redefine pred c1 = c2 means :: MEMBERED:def 11
for b1 being complex number holds
( b1 in a1 iff b1 in a2 );
compatibility
( c1 = c2 iff for b1 being complex number holds
( b1 in c1 iff b1 in c2 ) )
proof end;
end;

:: deftheorem Def11 defines = MEMBERED:def 11 :
for b1, b2 being complex-membered set holds
( b1 = b2 iff for b3 being complex number holds
( b3 in b1 iff b3 in b2 ) );

definition
let c1, c2 be real-membered set ;
redefine pred c1 = c2 means :: MEMBERED:def 12
for b1 being real number holds
( b1 in a1 iff b1 in a2 );
compatibility
( c1 = c2 iff for b1 being real number holds
( b1 in c1 iff b1 in c2 ) )
proof end;
end;

:: deftheorem Def12 defines = MEMBERED:def 12 :
for b1, b2 being real-membered set holds
( b1 = b2 iff for b3 being real number holds
( b3 in b1 iff b3 in b2 ) );

definition
let c1, c2 be rational-membered set ;
redefine pred c1 = c2 means :: MEMBERED:def 13
for b1 being rational number holds
( b1 in a1 iff b1 in a2 );
compatibility
( c1 = c2 iff for b1 being rational number holds
( b1 in c1 iff b1 in c2 ) )
proof end;
end;

:: deftheorem Def13 defines = MEMBERED:def 13 :
for b1, b2 being rational-membered set holds
( b1 = b2 iff for b3 being rational number holds
( b3 in b1 iff b3 in b2 ) );

definition
let c1, c2 be integer-membered set ;
redefine pred c1 = c2 means :: MEMBERED:def 14
for b1 being integer number holds
( b1 in a1 iff b1 in a2 );
compatibility
( c1 = c2 iff for b1 being integer number holds
( b1 in c1 iff b1 in c2 ) )
proof end;
end;

:: deftheorem Def14 defines = MEMBERED:def 14 :
for b1, b2 being integer-membered set holds
( b1 = b2 iff for b3 being integer number holds
( b3 in b1 iff b3 in b2 ) );

definition
let c1, c2 be natural-membered set ;
redefine pred c1 = c2 means :: MEMBERED:def 15
for b1 being natural number holds
( b1 in a1 iff b1 in a2 );
compatibility
( c1 = c2 iff for b1 being natural number holds
( b1 in c1 iff b1 in c2 ) )
proof end;
end;

:: deftheorem Def15 defines = MEMBERED:def 15 :
for b1, b2 being natural-membered set holds
( b1 = b2 iff for b3 being natural number holds
( b3 in b1 iff b3 in b2 ) );

definition
let c1, c2 be complex-membered set ;
redefine pred c1 misses c2 means :: MEMBERED:def 16
for b1 being complex number holds
( not b1 in a1 or not b1 in a2 );
compatibility
( not c1 meets c2 iff for b1 being complex number holds
( not b1 in c1 or not b1 in c2 ) )
proof end;
end;

:: deftheorem Def16 defines meets MEMBERED:def 16 :
for b1, b2 being complex-membered set holds
( not b1 meets b2 iff for b3 being complex number holds
( not b3 in b1 or not b3 in b2 ) );

definition
let c1, c2 be real-membered set ;
redefine pred c1 misses c2 means :: MEMBERED:def 17
for b1 being real number holds
( not b1 in a1 or not b1 in a2 );
compatibility
( not c1 meets c2 iff for b1 being real number holds
( not b1 in c1 or not b1 in c2 ) )
proof end;
end;

:: deftheorem Def17 defines meets MEMBERED:def 17 :
for b1, b2 being real-membered set holds
( not b1 meets b2 iff for b3 being real number holds
( not b3 in b1 or not b3 in b2 ) );

definition
let c1, c2 be rational-membered set ;
redefine pred c1 misses c2 means :: MEMBERED:def 18
for b1 being rational number holds
( not b1 in a1 or not b1 in a2 );
compatibility
( not c1 meets c2 iff for b1 being rational number holds
( not b1 in c1 or not b1 in c2 ) )
proof end;
end;

:: deftheorem Def18 defines meets MEMBERED:def 18 :
for b1, b2 being rational-membered set holds
( not b1 meets b2 iff for b3 being rational number holds
( not b3 in b1 or not b3 in b2 ) );

definition
let c1, c2 be integer-membered set ;
redefine pred c1 misses c2 means :: MEMBERED:def 19
for b1 being integer number holds
( not b1 in a1 or not b1 in a2 );
compatibility
( not c1 meets c2 iff for b1 being integer number holds
( not b1 in c1 or not b1 in c2 ) )
proof end;
end;

:: deftheorem Def19 defines meets MEMBERED:def 19 :
for b1, b2 being integer-membered set holds
( not b1 meets b2 iff for b3 being integer number holds
( not b3 in b1 or not b3 in b2 ) );

definition
let c1, c2 be natural-membered set ;
redefine pred c1 misses c2 means :: MEMBERED:def 20
for b1 being natural number holds
( not b1 in a1 or not b1 in a2 );
compatibility
( not c1 meets c2 iff for b1 being natural number holds
( not b1 in c1 or not b1 in c2 ) )
proof end;
end;

:: deftheorem Def20 defines meets MEMBERED:def 20 :
for b1, b2 being natural-membered set holds
( not b1 meets b2 iff for b3 being natural number holds
( not b3 in b1 or not b3 in b2 ) );

theorem Th21: :: MEMBERED:21
for b1 being set st ( for b2 being set st b2 in b1 holds
b2 is complex-membered ) holds
union b1 is complex-membered
proof end;

theorem Th22: :: MEMBERED:22
for b1 being set st ( for b2 being set st b2 in b1 holds
b2 is real-membered ) holds
union b1 is real-membered
proof end;

theorem Th23: :: MEMBERED:23
for b1 being set st ( for b2 being set st b2 in b1 holds
b2 is rational-membered ) holds
union b1 is rational-membered
proof end;

theorem Th24: :: MEMBERED:24
for b1 being set st ( for b2 being set st b2 in b1 holds
b2 is integer-membered ) holds
union b1 is integer-membered
proof end;

theorem Th25: :: MEMBERED:25
for b1 being set st ( for b2 being set st b2 in b1 holds
b2 is natural-membered ) holds
union b1 is natural-membered
proof end;

theorem Th26: :: MEMBERED:26
for b1, b2 being set st b2 in b1 & b2 is complex-membered holds
meet b1 is complex-membered
proof end;

theorem Th27: :: MEMBERED:27
for b1, b2 being set st b2 in b1 & b2 is real-membered holds
meet b1 is real-membered
proof end;

theorem Th28: :: MEMBERED:28
for b1, b2 being set st b2 in b1 & b2 is rational-membered holds
meet b1 is rational-membered
proof end;

theorem Th29: :: MEMBERED:29
for b1, b2 being set st b2 in b1 & b2 is integer-membered holds
meet b1 is integer-membered
proof end;

theorem Th30: :: MEMBERED:30
for b1, b2 being set st b2 in b1 & b2 is natural-membered holds
meet b1 is natural-membered
proof end;

scheme :: MEMBERED:sch 1
s1{ P1[ set ] } :
ex b1 being complex-membered set st
for b2 being complex number holds
( b2 in b1 iff P1[b2] )
proof end;

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

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

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

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