:: MEMBERED semantic presentation
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
proof
let X be set ; ::_thesis: ( X is natural-membered implies X is integer-membered )
assume A1: X is natural-membered ; ::_thesis: X is integer-membered
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in X implies x is integer )
assume x in X ; ::_thesis: x is integer
then x is natural by A1, Def6;
then x in omega by ORDINAL1:def_12;
hence x in INT by NUMBERS:17; :: according to INT_1:def_2 ::_thesis: verum
end;
cluster integer-membered -> rational-membered for set ;
coherence
for b1 being set st b1 is integer-membered holds
b1 is rational-membered
proof
let X be set ; ::_thesis: ( X is integer-membered implies X is rational-membered )
assume A2: X is integer-membered ; ::_thesis: X is rational-membered
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in X implies x is rational )
assume x in X ; ::_thesis: x is rational
then x is integer by A2, Def5;
then x in INT by INT_1:def_2;
hence x in RAT by NUMBERS:14; :: according to RAT_1:def_2 ::_thesis: verum
end;
cluster rational-membered -> real-membered for set ;
coherence
for b1 being set st b1 is rational-membered holds
b1 is real-membered
proof
let X be set ; ::_thesis: ( X is rational-membered implies X is real-membered )
assume A3: X is rational-membered ; ::_thesis: X is real-membered
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in X implies x is real )
assume x in X ; ::_thesis: x is real
then x is rational by A3, Def4;
then x in RAT by RAT_1:def_2;
hence x in REAL by NUMBERS:12; :: according to XREAL_0:def_1 ::_thesis: verum
end;
cluster real-membered -> ext-real-membered for set ;
coherence
for b1 being set st b1 is real-membered holds
b1 is ext-real-membered
proof
let X be set ; ::_thesis: ( X is real-membered implies X is ext-real-membered )
assume A4: X is real-membered ; ::_thesis: X is ext-real-membered
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in X implies x is ext-real )
assume x in X ; ::_thesis: x is ext-real
then x is real by A4, Def3;
then x in REAL by XREAL_0:def_1;
hence x in ExtREAL by NUMBERS:31; :: according to XXREAL_0:def_1 ::_thesis: verum
end;
cluster real-membered -> complex-membered for set ;
coherence
for b1 being set st b1 is real-membered holds
b1 is complex-membered
proof
let X be set ; ::_thesis: ( X is real-membered implies X is complex-membered )
assume A5: X is real-membered ; ::_thesis: X is complex-membered
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in X implies x is complex )
assume x in X ; ::_thesis: x is complex
then x is real by A5, Def3;
then x in REAL by XREAL_0:def_1;
hence x in COMPLEX by NUMBERS:11; :: according to XCMPLX_0:def_2 ::_thesis: verum
end;
end;
registration
cluster non empty natural-membered for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is natural-membered )
proof
take 1 ; ::_thesis: ( not 1 is empty & 1 is natural-membered )
thus not 1 is empty ; ::_thesis: 1 is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in 1 implies x is natural )
assume x in 1 ; ::_thesis: x is natural
hence x is natural by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
end;
registration
cluster -> complex-membered for Element of K18(COMPLEX);
coherence
for b1 being Subset of COMPLEX holds b1 is complex-membered
proof
let S be Subset of COMPLEX; ::_thesis: S is complex-membered
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in S implies x is complex )
thus ( x in S implies x is complex ) ; ::_thesis: verum
end;
cluster -> ext-real-membered for Element of K18(ExtREAL);
coherence
for b1 being Subset of ExtREAL holds b1 is ext-real-membered
proof
let S be Subset of ExtREAL; ::_thesis: S is ext-real-membered
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in S implies x is ext-real )
thus ( x in S implies x is ext-real ) by XXREAL_0:def_1; ::_thesis: verum
end;
cluster -> real-membered for Element of K18(REAL);
coherence
for b1 being Subset of REAL holds b1 is real-membered
proof
let S be Subset of REAL; ::_thesis: S is real-membered
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in S implies x is real )
thus ( x in S implies x is real ) ; ::_thesis: verum
end;
cluster -> rational-membered for Element of K18(RAT);
coherence
for b1 being Subset of RAT holds b1 is rational-membered
proof
let S be Subset of RAT; ::_thesis: S is rational-membered
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in S implies x is rational )
thus ( x in S implies x is rational ) by RAT_1:def_2; ::_thesis: verum
end;
cluster -> integer-membered for Element of K18(INT);
coherence
for b1 being Subset of INT holds b1 is integer-membered
proof
let S be Subset of INT; ::_thesis: S is integer-membered
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in S implies x is integer )
thus ( x in S implies x is integer ) ; ::_thesis: verum
end;
cluster -> natural-membered for Element of K18(NAT);
coherence
for b1 being Subset of NAT holds b1 is natural-membered
proof
let S be Subset of NAT; ::_thesis: S is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in S implies x is natural )
thus ( x in S implies x is natural ) ; ::_thesis: verum
end;
end;
registration
cluster COMPLEX -> complex-membered ;
coherence
COMPLEX is complex-membered
proof
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in COMPLEX implies x is complex )
thus ( x in COMPLEX implies x is complex ) ; ::_thesis: verum
end;
cluster ExtREAL -> ext-real-membered ;
coherence
ExtREAL is ext-real-membered
proof
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in ExtREAL implies x is ext-real )
thus ( x in ExtREAL implies x is ext-real ) by XXREAL_0:def_1; ::_thesis: verum
end;
cluster REAL -> real-membered ;
coherence
REAL is real-membered
proof
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in REAL implies x is real )
thus ( x in REAL implies x is real ) ; ::_thesis: verum
end;
cluster RAT -> rational-membered ;
coherence
RAT is rational-membered
proof
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in RAT implies x is rational )
thus ( x in RAT implies x is rational ) by RAT_1:def_2; ::_thesis: verum
end;
cluster INT -> integer-membered ;
coherence
INT is integer-membered
proof
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in INT implies x is integer )
thus ( x in INT implies x is integer ) ; ::_thesis: verum
end;
cluster NAT -> natural-membered ;
coherence
NAT is natural-membered
proof
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in NAT implies x is natural )
thus ( x in NAT implies x is natural ) ; ::_thesis: verum
end;
end;
theorem Th1: :: MEMBERED:1
for X being set st X is complex-membered holds
X c= COMPLEX
proof
let X be set ; ::_thesis: ( X is complex-membered implies X c= COMPLEX )
assume A1: X is complex-membered ; ::_thesis: X c= COMPLEX
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in COMPLEX )
assume x in X ; ::_thesis: x in COMPLEX
then x is complex by A1, Def1;
hence x in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
theorem Th2: :: MEMBERED:2
for X being set st X is ext-real-membered holds
X c= ExtREAL
proof
let X be set ; ::_thesis: ( X is ext-real-membered implies X c= ExtREAL )
assume A1: X is ext-real-membered ; ::_thesis: X c= ExtREAL
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in ExtREAL )
assume x in X ; ::_thesis: x in ExtREAL
then x is ext-real by A1, Def2;
hence x in ExtREAL by XXREAL_0:def_1; ::_thesis: verum
end;
theorem Th3: :: MEMBERED:3
for X being set st X is real-membered holds
X c= REAL
proof
let X be set ; ::_thesis: ( X is real-membered implies X c= REAL )
assume A1: X is real-membered ; ::_thesis: X c= REAL
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in REAL )
assume x in X ; ::_thesis: x in REAL
then x is real by A1, Def3;
hence x in REAL by XREAL_0:def_1; ::_thesis: verum
end;
theorem Th4: :: MEMBERED:4
for X being set st X is rational-membered holds
X c= RAT
proof
let X be set ; ::_thesis: ( X is rational-membered implies X c= RAT )
assume A1: X is rational-membered ; ::_thesis: X c= RAT
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in RAT )
assume x in X ; ::_thesis: x in RAT
then x is rational by A1, Def4;
hence x in RAT by RAT_1:def_2; ::_thesis: verum
end;
theorem Th5: :: MEMBERED:5
for X being set st X is integer-membered holds
X c= INT
proof
let X be set ; ::_thesis: ( X is integer-membered implies X c= INT )
assume A1: X is integer-membered ; ::_thesis: X c= INT
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in INT )
assume x in X ; ::_thesis: x in INT
then x is integer by A1, Def5;
hence x in INT by INT_1:def_2; ::_thesis: verum
end;
theorem Th6: :: MEMBERED:6
for X being set st X is natural-membered holds
X c= NAT
proof
let X be set ; ::_thesis: ( X is natural-membered implies X c= NAT )
assume A1: X is natural-membered ; ::_thesis: X c= NAT
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in NAT )
assume x in X ; ::_thesis: x in NAT
then x is natural by A1, Def6;
hence x in NAT by ORDINAL1:def_12; ::_thesis: verum
end;
registration
let X be complex-membered set ;
cluster -> complex for Element of X;
coherence
for b1 being Element of X holds b1 is complex
proof
let e be Element of X; ::_thesis: e is complex
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: e is complex
hence e is complex by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: e is complex
hence e is complex by Def1; ::_thesis: verum
end;
end;
end;
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
proof
let e be Element of X; ::_thesis: e is ext-real
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: e is ext-real
hence e is ext-real by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: e is ext-real
hence e is ext-real by Def2; ::_thesis: verum
end;
end;
end;
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
proof
let e be Element of X; ::_thesis: e is real
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: e is real
hence e is real by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: e is real
hence e is real by Def3; ::_thesis: verum
end;
end;
end;
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
proof
let e be Element of X; ::_thesis: e is rational
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: e is rational
hence e is rational by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: e is rational
hence e is rational by Def4; ::_thesis: verum
end;
end;
end;
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
proof
let e be Element of X; ::_thesis: e is integer
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: e is integer
hence e is integer by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: e is integer
hence e is integer by Def5; ::_thesis: verum
end;
end;
end;
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
proof
let e be Element of X; ::_thesis: e is natural
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: e is natural
hence e is natural by SUBSET_1:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: e is natural
hence e is natural by Def6; ::_thesis: verum
end;
end;
end;
end;
theorem :: MEMBERED:7
for X being non empty complex-membered set ex c being complex number st c in X
proof
let X be non empty complex-membered set ; ::_thesis: ex c being complex number st c in X
ex x being set st x in X by XBOOLE_0:def_1;
hence ex c being complex number st c in X ; ::_thesis: verum
end;
theorem :: MEMBERED:8
for X being non empty ext-real-membered set ex e being ext-real number st e in X
proof
let X be non empty ext-real-membered set ; ::_thesis: ex e being ext-real number st e in X
ex x being set st x in X by XBOOLE_0:def_1;
hence ex e being ext-real number st e in X ; ::_thesis: verum
end;
theorem :: MEMBERED:9
for X being non empty real-membered set ex r being real number st r in X
proof
let X be non empty real-membered set ; ::_thesis: ex r being real number st r in X
ex x being set st x in X by XBOOLE_0:def_1;
hence ex r being real number st r in X ; ::_thesis: verum
end;
theorem :: MEMBERED:10
for X being non empty rational-membered set ex w being rational number st w in X
proof
let X be non empty rational-membered set ; ::_thesis: ex w being rational number st w in X
ex x being set st x in X by XBOOLE_0:def_1;
hence ex w being rational number st w in X ; ::_thesis: verum
end;
theorem :: MEMBERED:11
for X being non empty integer-membered set ex i being integer number st i in X
proof
let X be non empty integer-membered set ; ::_thesis: ex i being integer number st i in X
ex x being set st x in X by XBOOLE_0:def_1;
hence ex i being integer number st i in X ; ::_thesis: verum
end;
theorem :: MEMBERED:12
for X being non empty natural-membered set ex n being Nat st n in X
proof
let X be non empty natural-membered set ; ::_thesis: ex n being Nat st n in X
ex x being set st x in X by XBOOLE_0:def_1;
hence ex n being Nat st n in X ; ::_thesis: verum
end;
theorem :: MEMBERED:13
for X being complex-membered set st ( for c being complex number holds c in X ) holds
X = COMPLEX
proof
let X be complex-membered set ; ::_thesis: ( ( for c being complex number holds c in X ) implies X = COMPLEX )
assume A1: for c being complex number holds c in X ; ::_thesis: X = COMPLEX
thus X c= COMPLEX by Th1; :: according to XBOOLE_0:def_10 ::_thesis: COMPLEX c= X
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in COMPLEX or e in X )
assume e in COMPLEX ; ::_thesis: e in X
hence e in X by A1; ::_thesis: verum
end;
theorem :: MEMBERED:14
for X being ext-real-membered set st ( for e being ext-real number holds e in X ) holds
X = ExtREAL
proof
let X be ext-real-membered set ; ::_thesis: ( ( for e being ext-real number holds e in X ) implies X = ExtREAL )
assume A1: for e being ext-real number holds e in X ; ::_thesis: X = ExtREAL
thus X c= ExtREAL by Th2; :: according to XBOOLE_0:def_10 ::_thesis: ExtREAL c= X
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ExtREAL or e in X )
assume e in ExtREAL ; ::_thesis: e in X
hence e in X by A1; ::_thesis: verum
end;
theorem :: MEMBERED:15
for X being real-membered set st ( for r being real number holds r in X ) holds
X = REAL
proof
let X be real-membered set ; ::_thesis: ( ( for r being real number holds r in X ) implies X = REAL )
assume A1: for r being real number holds r in X ; ::_thesis: X = REAL
thus X c= REAL by Th3; :: according to XBOOLE_0:def_10 ::_thesis: REAL c= X
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in REAL or e in X )
assume e in REAL ; ::_thesis: e in X
hence e in X by A1; ::_thesis: verum
end;
theorem :: MEMBERED:16
for X being rational-membered set st ( for w being rational number holds w in X ) holds
X = RAT
proof
let X be rational-membered set ; ::_thesis: ( ( for w being rational number holds w in X ) implies X = RAT )
assume A1: for w being rational number holds w in X ; ::_thesis: X = RAT
thus X c= RAT by Th4; :: according to XBOOLE_0:def_10 ::_thesis: RAT c= X
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in RAT or e in X )
assume e in RAT ; ::_thesis: e in X
hence e in X by A1; ::_thesis: verum
end;
theorem :: MEMBERED:17
for X being integer-membered set st ( for i being integer number holds i in X ) holds
X = INT
proof
let X be integer-membered set ; ::_thesis: ( ( for i being integer number holds i in X ) implies X = INT )
assume A1: for i being integer number holds i in X ; ::_thesis: X = INT
thus X c= INT by Th5; :: according to XBOOLE_0:def_10 ::_thesis: INT c= X
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in INT or e in X )
assume e in INT ; ::_thesis: e in X
hence e in X by A1; ::_thesis: verum
end;
theorem :: MEMBERED:18
for X being natural-membered set st ( for n being Nat holds n in X ) holds
X = NAT
proof
let X be natural-membered set ; ::_thesis: ( ( for n being Nat holds n in X ) implies X = NAT )
assume A1: for n being Nat holds n in X ; ::_thesis: X = NAT
thus X c= NAT by Th6; :: according to XBOOLE_0:def_10 ::_thesis: NAT c= X
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in NAT or e in X )
assume e in NAT ; ::_thesis: e in X
hence e in X by A1; ::_thesis: verum
end;
theorem Th19: :: MEMBERED:19
for X being set
for Y being complex-membered set st X c= Y holds
X is complex-membered
proof
let X be set ; ::_thesis: for Y being complex-membered set st X c= Y holds
X is complex-membered
let Y be complex-membered set ; ::_thesis: ( X c= Y implies X is complex-membered )
assume A1: X c= Y ; ::_thesis: X is complex-membered
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in X implies x is complex )
thus ( x in X implies x is complex ) by A1; ::_thesis: verum
end;
theorem Th20: :: MEMBERED:20
for X being set
for Y being ext-real-membered set st X c= Y holds
X is ext-real-membered
proof
let X be set ; ::_thesis: for Y being ext-real-membered set st X c= Y holds
X is ext-real-membered
let Y be ext-real-membered set ; ::_thesis: ( X c= Y implies X is ext-real-membered )
assume A1: X c= Y ; ::_thesis: X is ext-real-membered
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in X implies x is ext-real )
thus ( x in X implies x is ext-real ) by A1; ::_thesis: verum
end;
theorem Th21: :: MEMBERED:21
for X being set
for Y being real-membered set st X c= Y holds
X is real-membered
proof
let X be set ; ::_thesis: for Y being real-membered set st X c= Y holds
X is real-membered
let Y be real-membered set ; ::_thesis: ( X c= Y implies X is real-membered )
assume A1: X c= Y ; ::_thesis: X is real-membered
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in X implies x is real )
thus ( x in X implies x is real ) by A1; ::_thesis: verum
end;
theorem Th22: :: MEMBERED:22
for X being set
for Y being rational-membered set st X c= Y holds
X is rational-membered
proof
let X be set ; ::_thesis: for Y being rational-membered set st X c= Y holds
X is rational-membered
let Y be rational-membered set ; ::_thesis: ( X c= Y implies X is rational-membered )
assume A1: X c= Y ; ::_thesis: X is rational-membered
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in X implies x is rational )
thus ( x in X implies x is rational ) by A1; ::_thesis: verum
end;
theorem Th23: :: MEMBERED:23
for X being set
for Y being integer-membered set st X c= Y holds
X is integer-membered
proof
let X be set ; ::_thesis: for Y being integer-membered set st X c= Y holds
X is integer-membered
let Y be integer-membered set ; ::_thesis: ( X c= Y implies X is integer-membered )
assume A1: X c= Y ; ::_thesis: X is integer-membered
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in X implies x is integer )
thus ( x in X implies x is integer ) by A1; ::_thesis: verum
end;
theorem Th24: :: MEMBERED:24
for X being set
for Y being natural-membered set st X c= Y holds
X is natural-membered
proof
let X be set ; ::_thesis: for Y being natural-membered set st X c= Y holds
X is natural-membered
let Y be natural-membered set ; ::_thesis: ( X c= Y implies X is natural-membered )
assume A1: X c= Y ; ::_thesis: X is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in X implies x is natural )
thus ( x in X implies x is natural ) by A1; ::_thesis: verum
end;
registration
cluster empty -> natural-membered for set ;
coherence
for b1 being set st b1 is empty holds
b1 is natural-membered
proof
let X be set ; ::_thesis: ( X is empty implies X is natural-membered )
assume A1: X is empty ; ::_thesis: X is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in X implies x is natural )
thus ( x in X implies x is natural ) by A1; ::_thesis: verum
end;
end;
registration
let c be complex number ;
cluster{c} -> complex-membered ;
coherence
{c} is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( e in {c} implies e is complex )
thus ( e in {c} implies e is complex ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let e be ext-real number ;
cluster{e} -> ext-real-membered ;
coherence
{e} is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( e in {e} implies e is ext-real )
thus ( e in {e} implies e is ext-real ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let r be real number ;
cluster{r} -> real-membered ;
coherence
{r} is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( e in {r} implies e is real )
thus ( e in {r} implies e is real ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let w be rational number ;
cluster{w} -> rational-membered ;
coherence
{w} is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( e in {w} implies e is rational )
thus ( e in {w} implies e is rational ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let i be integer number ;
cluster{i} -> integer-membered ;
coherence
{i} is integer-membered
proof
let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( e in {i} implies e is integer )
thus ( e in {i} implies e is integer ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster{n} -> natural-membered ;
coherence
{n} is natural-membered
proof
let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( e in {n} implies e is natural )
thus ( e in {n} implies e is natural ) by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let c1, c2 be complex number ;
cluster{c1,c2} -> complex-membered ;
coherence
{c1,c2} is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( e in {c1,c2} implies e is complex )
thus ( e in {c1,c2} implies e is complex ) by TARSKI:def_2; ::_thesis: verum
end;
end;
registration
let e1, e2 be ext-real number ;
cluster{e1,e2} -> ext-real-membered ;
coherence
{e1,e2} is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( e in {e1,e2} implies e is ext-real )
thus ( e in {e1,e2} implies e is ext-real ) by TARSKI:def_2; ::_thesis: verum
end;
end;
registration
let r1, r2 be real number ;
cluster{r1,r2} -> real-membered ;
coherence
{r1,r2} is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( e in {r1,r2} implies e is real )
thus ( e in {r1,r2} implies e is real ) by TARSKI:def_2; ::_thesis: verum
end;
end;
registration
let w1, w2 be rational number ;
cluster{w1,w2} -> rational-membered ;
coherence
{w1,w2} is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( e in {w1,w2} implies e is rational )
thus ( e in {w1,w2} implies e is rational ) by TARSKI:def_2; ::_thesis: verum
end;
end;
registration
let i1, i2 be integer number ;
cluster{i1,i2} -> integer-membered ;
coherence
{i1,i2} is integer-membered
proof
let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( e in {i1,i2} implies e is integer )
thus ( e in {i1,i2} implies e is integer ) by TARSKI:def_2; ::_thesis: verum
end;
end;
registration
let n1, n2 be Nat;
cluster{n1,n2} -> natural-membered ;
coherence
{n1,n2} is natural-membered
proof
let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( e in {n1,n2} implies e is natural )
thus ( e in {n1,n2} implies e is natural ) by TARSKI:def_2; ::_thesis: verum
end;
end;
registration
let c1, c2, c3 be complex number ;
cluster{c1,c2,c3} -> complex-membered ;
coherence
{c1,c2,c3} is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( e in {c1,c2,c3} implies e is complex )
thus ( e in {c1,c2,c3} implies e is complex ) by ENUMSET1:def_1; ::_thesis: verum
end;
end;
registration
let e1, e2, e3 be ext-real number ;
cluster{e1,e2,e3} -> ext-real-membered ;
coherence
{e1,e2,e3} is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( e in {e1,e2,e3} implies e is ext-real )
thus ( e in {e1,e2,e3} implies e is ext-real ) by ENUMSET1:def_1; ::_thesis: verum
end;
end;
registration
let r1, r2, r3 be real number ;
cluster{r1,r2,r3} -> real-membered ;
coherence
{r1,r2,r3} is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( e in {r1,r2,r3} implies e is real )
thus ( e in {r1,r2,r3} implies e is real ) by ENUMSET1:def_1; ::_thesis: verum
end;
end;
registration
let w1, w2, w3 be rational number ;
cluster{w1,w2,w3} -> rational-membered ;
coherence
{w1,w2,w3} is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( e in {w1,w2,w3} implies e is rational )
thus ( e in {w1,w2,w3} implies e is rational ) by ENUMSET1:def_1; ::_thesis: verum
end;
end;
registration
let i1, i2, i3 be integer number ;
cluster{i1,i2,i3} -> integer-membered ;
coherence
{i1,i2,i3} is integer-membered
proof
let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( e in {i1,i2,i3} implies e is integer )
thus ( e in {i1,i2,i3} implies e is integer ) by ENUMSET1:def_1; ::_thesis: verum
end;
end;
registration
let n1, n2, n3 be Nat;
cluster{n1,n2,n3} -> natural-membered ;
coherence
{n1,n2,n3} is natural-membered
proof
let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( e in {n1,n2,n3} implies e is natural )
thus ( e in {n1,n2,n3} implies e is natural ) by ENUMSET1:def_1; ::_thesis: verum
end;
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
proof
let S be Subset of X; ::_thesis: S is complex-membered
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in S implies x is complex )
thus ( x in S implies x is complex ) ; ::_thesis: verum
end;
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
proof
let S be Subset of X; ::_thesis: S is ext-real-membered
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in S implies x is ext-real )
thus ( x in S implies x is ext-real ) ; ::_thesis: verum
end;
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
proof
let S be Subset of X; ::_thesis: S is real-membered
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in S implies x is real )
thus ( x in S implies x is real ) ; ::_thesis: verum
end;
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
proof
let S be Subset of X; ::_thesis: S is rational-membered
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in S implies x is rational )
thus ( x in S implies x is rational ) ; ::_thesis: verum
end;
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
proof
let S be Subset of X; ::_thesis: S is integer-membered
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in S implies x is integer )
thus ( x in S implies x is integer ) ; ::_thesis: verum
end;
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
proof
let S be Subset of X; ::_thesis: S is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in S implies x is natural )
thus ( x in S implies x is natural ) ; ::_thesis: verum
end;
end;
registration
let X, Y be complex-membered set ;
clusterX \/ Y -> complex-membered ;
coherence
X \/ Y is complex-membered
proof
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in X \/ Y implies x is complex )
assume x in X \/ Y ; ::_thesis: x is complex
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is complex ; ::_thesis: verum
end;
end;
registration
let X, Y be ext-real-membered set ;
clusterX \/ Y -> ext-real-membered ;
coherence
X \/ Y is ext-real-membered
proof
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in X \/ Y implies x is ext-real )
assume x in X \/ Y ; ::_thesis: x is ext-real
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is ext-real ; ::_thesis: verum
end;
end;
registration
let X, Y be real-membered set ;
clusterX \/ Y -> real-membered ;
coherence
X \/ Y is real-membered
proof
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in X \/ Y implies x is real )
assume x in X \/ Y ; ::_thesis: x is real
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is real ; ::_thesis: verum
end;
end;
registration
let X, Y be rational-membered set ;
clusterX \/ Y -> rational-membered ;
coherence
X \/ Y is rational-membered
proof
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in X \/ Y implies x is rational )
assume x in X \/ Y ; ::_thesis: x is rational
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is rational ; ::_thesis: verum
end;
end;
registration
let X, Y be integer-membered set ;
clusterX \/ Y -> integer-membered ;
coherence
X \/ Y is integer-membered
proof
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in X \/ Y implies x is integer )
assume x in X \/ Y ; ::_thesis: x is integer
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is integer ; ::_thesis: verum
end;
end;
registration
let X, Y be natural-membered set ;
clusterX \/ Y -> natural-membered ;
coherence
X \/ Y is natural-membered
proof
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in X \/ Y implies x is natural )
assume x in X \/ Y ; ::_thesis: x is natural
then ( x in X or x in Y ) by XBOOLE_0:def_3;
hence x is natural ; ::_thesis: verum
end;
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 )
proof
thus ( X c= Y implies for c being complex number st c in X holds
c in Y ) ; ::_thesis: ( ( for c being complex number st c in X holds
c in Y ) implies X c= Y )
assume A1: for c being complex number st c in X holds
c in Y ; ::_thesis: X c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y )
assume x in X ; ::_thesis: x in Y
hence x in Y by A1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines c= MEMBERED:def_7_:_
for X being complex-membered set
for Y being set holds
( X c= Y iff for c being complex number st c in X holds
c in Y );
definition
let X be ext-real-membered set ;
let Y be set ;
redefine pred X c= Y means :Def8: :: MEMBERED:def 8
for e being ext-real number st e in X holds
e in Y;
compatibility
( X c= Y iff for e being ext-real number st e in X holds
e in Y )
proof
thus ( X c= Y implies for e being ext-real number st e in X holds
e in Y ) ; ::_thesis: ( ( for e being ext-real number st e in X holds
e in Y ) implies X c= Y )
assume A1: for e being ext-real number st e in X holds
e in Y ; ::_thesis: X c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y )
assume x in X ; ::_thesis: x in Y
hence x in Y by A1; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines c= MEMBERED:def_8_:_
for X being ext-real-membered set
for Y being set holds
( X c= Y iff for e being ext-real number st e in X holds
e in Y );
definition
let X be real-membered set ;
let Y be set ;
redefine pred X c= Y means :Def9: :: MEMBERED:def 9
for r being real number st r in X holds
r in Y;
compatibility
( X c= Y iff for r being real number st r in X holds
r in Y )
proof
thus ( X c= Y implies for r being real number st r in X holds
r in Y ) ; ::_thesis: ( ( for r being real number st r in X holds
r in Y ) implies X c= Y )
assume A1: for r being real number st r in X holds
r in Y ; ::_thesis: X c= Y
let e be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( e in X implies e in Y )
assume e in X ; ::_thesis: e in Y
hence e in Y by A1; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines c= MEMBERED:def_9_:_
for X being real-membered set
for Y being set holds
( X c= Y iff for r being real number st r in X holds
r in Y );
definition
let X be rational-membered set ;
let Y be set ;
redefine pred X c= Y means :Def10: :: MEMBERED:def 10
for w being rational number st w in X holds
w in Y;
compatibility
( X c= Y iff for w being rational number st w in X holds
w in Y )
proof
thus ( X c= Y implies for w being rational number st w in X holds
w in Y ) ; ::_thesis: ( ( for w being rational number st w in X holds
w in Y ) implies X c= Y )
assume A1: for w being rational number st w in X holds
w in Y ; ::_thesis: X c= Y
let r be real number ; :: according to MEMBERED:def_9 ::_thesis: ( r in X implies r in Y )
assume r in X ; ::_thesis: r in Y
hence r in Y by A1; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines c= MEMBERED:def_10_:_
for X being rational-membered set
for Y being set holds
( X c= Y iff for w being rational number st w in X holds
w in Y );
definition
let X be integer-membered set ;
let Y be set ;
redefine pred X c= Y means :Def11: :: MEMBERED:def 11
for i being integer number st i in X holds
i in Y;
compatibility
( X c= Y iff for i being integer number st i in X holds
i in Y )
proof
thus ( X c= Y implies for i being integer number st i in X holds
i in Y ) ; ::_thesis: ( ( for i being integer number st i in X holds
i in Y ) implies X c= Y )
assume A1: for i being integer number st i in X holds
i in Y ; ::_thesis: X c= Y
let w be rational number ; :: according to MEMBERED:def_10 ::_thesis: ( w in X implies w in Y )
assume w in X ; ::_thesis: w in Y
hence w in Y by A1; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines c= MEMBERED:def_11_:_
for X being integer-membered set
for Y being set holds
( X c= Y iff for i being integer number st i in X holds
i in Y );
definition
let X be natural-membered set ;
let Y be set ;
redefine pred X c= Y means :Def12: :: MEMBERED:def 12
for n being Nat st n in X holds
n in Y;
compatibility
( X c= Y iff for n being Nat st n in X holds
n in Y )
proof
thus ( X c= Y implies for n being Nat st n in X holds
n in Y ) ; ::_thesis: ( ( for n being Nat st n in X holds
n in Y ) implies X c= Y )
assume A1: for n being Nat st n in X holds
n in Y ; ::_thesis: X c= Y
let i be integer number ; :: according to MEMBERED:def_11 ::_thesis: ( i in X implies i in Y )
assume i in X ; ::_thesis: i in Y
hence i in Y by A1; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines c= MEMBERED:def_12_:_
for X being natural-membered set
for Y being set holds
( X c= Y iff for n being Nat st n in X holds
n in Y );
definition
let X, Y be complex-membered set ;
redefine pred X = Y means :: MEMBERED:def 13
for c being complex number holds
( c in X iff c in Y );
compatibility
( X = Y iff for c being complex number holds
( c in X iff c in Y ) )
proof
thus ( X = Y implies for c being complex number holds
( c in X iff c in Y ) ) ; ::_thesis: ( ( for c being complex number holds
( c in X iff c in Y ) ) implies X = Y )
assume for c being complex number holds
( c in X iff c in Y ) ; ::_thesis: X = Y
hence ( X c= Y & Y c= X ) by Def7; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;
:: deftheorem defines = MEMBERED:def_13_:_
for X, Y being complex-membered set holds
( X = Y iff for c being complex number holds
( c in X iff c in Y ) );
definition
let X, Y be ext-real-membered set ;
redefine pred X = Y means :: MEMBERED:def 14
for e being ext-real number holds
( e in X iff e in Y );
compatibility
( X = Y iff for e being ext-real number holds
( e in X iff e in Y ) )
proof
thus ( X = Y implies for e being ext-real number holds
( e in X iff e in Y ) ) ; ::_thesis: ( ( for e being ext-real number holds
( e in X iff e in Y ) ) implies X = Y )
assume for e being ext-real number holds
( e in X iff e in Y ) ; ::_thesis: X = Y
then ( X c= Y & Y c= X ) by Def8;
hence X = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines = MEMBERED:def_14_:_
for X, Y being ext-real-membered set holds
( X = Y iff for e being ext-real number holds
( e in X iff e in Y ) );
definition
let X, Y be real-membered set ;
redefine pred X = Y means :: MEMBERED:def 15
for r being real number holds
( r in X iff r in Y );
compatibility
( X = Y iff for r being real number holds
( r in X iff r in Y ) )
proof
thus ( X = Y implies for r being real number holds
( r in X iff r in Y ) ) ; ::_thesis: ( ( for r being real number holds
( r in X iff r in Y ) ) implies X = Y )
assume for r being real number holds
( r in X iff r in Y ) ; ::_thesis: X = Y
then ( X c= Y & Y c= X ) by Def9;
hence X = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines = MEMBERED:def_15_:_
for X, Y being real-membered set holds
( X = Y iff for r being real number holds
( r in X iff r in Y ) );
definition
let X, Y be rational-membered set ;
redefine pred X = Y means :: MEMBERED:def 16
for w being rational number holds
( w in X iff w in Y );
compatibility
( X = Y iff for w being rational number holds
( w in X iff w in Y ) )
proof
thus ( X = Y implies for w being rational number holds
( w in X iff w in Y ) ) ; ::_thesis: ( ( for w being rational number holds
( w in X iff w in Y ) ) implies X = Y )
assume for w being rational number holds
( w in X iff w in Y ) ; ::_thesis: X = Y
then ( X c= Y & Y c= X ) by Def10;
hence X = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines = MEMBERED:def_16_:_
for X, Y being rational-membered set holds
( X = Y iff for w being rational number holds
( w in X iff w in Y ) );
definition
let X, Y be integer-membered set ;
redefine pred X = Y means :: MEMBERED:def 17
for i being integer number holds
( i in X iff i in Y );
compatibility
( X = Y iff for i being integer number holds
( i in X iff i in Y ) )
proof
thus ( X = Y implies for i being integer number holds
( i in X iff i in Y ) ) ; ::_thesis: ( ( for i being integer number holds
( i in X iff i in Y ) ) implies X = Y )
assume for i being integer number holds
( i in X iff i in Y ) ; ::_thesis: X = Y
then ( X c= Y & Y c= X ) by Def11;
hence X = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines = MEMBERED:def_17_:_
for X, Y being integer-membered set holds
( X = Y iff for i being integer number holds
( i in X iff i in Y ) );
definition
let X, Y be natural-membered set ;
redefine pred X = Y means :: MEMBERED:def 18
for n being Nat holds
( n in X iff n in Y );
compatibility
( X = Y iff for n being Nat holds
( n in X iff n in Y ) )
proof
thus ( X = Y implies for n being Nat holds
( n in X iff n in Y ) ) ; ::_thesis: ( ( for n being Nat holds
( n in X iff n in Y ) ) implies X = Y )
assume for n being Nat holds
( n in X iff n in Y ) ; ::_thesis: X = Y
then ( X c= Y & Y c= X ) by Def12;
hence X = Y by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines = MEMBERED:def_18_:_
for X, Y being natural-membered set holds
( X = Y iff for n being Nat holds
( n in X iff n in Y ) );
definition
let X, Y be complex-membered set ;
redefine pred X misses Y means :: MEMBERED:def 19
for c being complex number holds
( not c in X or not c in Y );
compatibility
( not X meets Y iff for c being complex number holds
( not c in X or not c in Y ) )
proof
thus ( X misses Y implies for c being complex number holds
( not c in X or not c in Y ) ) by XBOOLE_0:3; ::_thesis: ( ( for c being complex number holds
( not c in X or not c in Y ) ) implies not X meets Y )
assume A1: for c being complex number holds
( not c in X or not c in Y ) ; ::_thesis: not X meets Y
assume X meets Y ; ::_thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem defines meets MEMBERED:def_19_:_
for X, Y being complex-membered set holds
( not X meets Y iff for c being complex number holds
( not c in X or not c in Y ) );
definition
let X, Y be ext-real-membered set ;
redefine pred X misses Y means :: MEMBERED:def 20
for e being ext-real number holds
( not e in X or not e in Y );
compatibility
( not X meets Y iff for e being ext-real number holds
( not e in X or not e in Y ) )
proof
thus ( X misses Y implies for e being ext-real number holds
( not e in X or not e in Y ) ) by XBOOLE_0:3; ::_thesis: ( ( for e being ext-real number holds
( not e in X or not e in Y ) ) implies not X meets Y )
assume A1: for e being ext-real number holds
( not e in X or not e in Y ) ; ::_thesis: not X meets Y
assume X meets Y ; ::_thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem defines meets MEMBERED:def_20_:_
for X, Y being ext-real-membered set holds
( not X meets Y iff for e being ext-real number holds
( not e in X or not e in Y ) );
definition
let X, Y be real-membered set ;
redefine pred X misses Y means :: MEMBERED:def 21
for r being real number holds
( not r in X or not r in Y );
compatibility
( not X meets Y iff for r being real number holds
( not r in X or not r in Y ) )
proof
thus ( X misses Y implies for r being real number holds
( not r in X or not r in Y ) ) by XBOOLE_0:3; ::_thesis: ( ( for r being real number holds
( not r in X or not r in Y ) ) implies not X meets Y )
assume A1: for r being real number holds
( not r in X or not r in Y ) ; ::_thesis: not X meets Y
assume X meets Y ; ::_thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem defines meets MEMBERED:def_21_:_
for X, Y being real-membered set holds
( not X meets Y iff for r being real number holds
( not r in X or not r in Y ) );
definition
let X, Y be rational-membered set ;
redefine pred X misses Y means :: MEMBERED:def 22
for w being rational number holds
( not w in X or not w in Y );
compatibility
( not X meets Y iff for w being rational number holds
( not w in X or not w in Y ) )
proof
thus ( X misses Y implies for w being rational number holds
( not w in X or not w in Y ) ) by XBOOLE_0:3; ::_thesis: ( ( for w being rational number holds
( not w in X or not w in Y ) ) implies not X meets Y )
assume A1: for w being rational number holds
( not w in X or not w in Y ) ; ::_thesis: not X meets Y
assume X meets Y ; ::_thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem defines meets MEMBERED:def_22_:_
for X, Y being rational-membered set holds
( not X meets Y iff for w being rational number holds
( not w in X or not w in Y ) );
definition
let X, Y be integer-membered set ;
redefine pred X misses Y means :: MEMBERED:def 23
for i being integer number holds
( not i in X or not i in Y );
compatibility
( not X meets Y iff for i being integer number holds
( not i in X or not i in Y ) )
proof
thus ( X misses Y implies for i being integer number holds
( not i in X or not i in Y ) ) by XBOOLE_0:3; ::_thesis: ( ( for i being integer number holds
( not i in X or not i in Y ) ) implies not X meets Y )
assume A1: for i being integer number holds
( not i in X or not i in Y ) ; ::_thesis: not X meets Y
assume X meets Y ; ::_thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem defines meets MEMBERED:def_23_:_
for X, Y being integer-membered set holds
( not X meets Y iff for i being integer number holds
( not i in X or not i in Y ) );
definition
let X, Y be natural-membered set ;
redefine pred X misses Y means :: MEMBERED:def 24
for n being Nat holds
( not n in X or not n in Y );
compatibility
( not X meets Y iff for n being Nat holds
( not n in X or not n in Y ) )
proof
thus ( X misses Y implies for n being Nat holds
( not n in X or not n in Y ) ) by XBOOLE_0:3; ::_thesis: ( ( for n being Nat holds
( not n in X or not n in Y ) ) implies not X meets Y )
assume A1: for n being Nat holds
( not n in X or not n in Y ) ; ::_thesis: not X meets Y
assume X meets Y ; ::_thesis: contradiction
then ex x being set st
( x in X & x in Y ) by XBOOLE_0:3;
hence contradiction by A1; ::_thesis: verum
end;
end;
:: deftheorem defines meets MEMBERED:def_24_:_
for X, Y being natural-membered set holds
( not X meets Y iff for n being Nat holds
( not n in X or not n in Y ) );
theorem :: MEMBERED:25
for F being set st ( for X being set st X in F holds
X is complex-membered ) holds
union F is complex-membered
proof
let F be set ; ::_thesis: ( ( for X being set st X in F holds
X is complex-membered ) implies union F is complex-membered )
assume A1: for X being set st X in F holds
X is complex-membered ; ::_thesis: union F is complex-membered
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in union F implies x is complex )
assume x in union F ; ::_thesis: x is complex
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def_4;
X is complex-membered by A1, A3;
hence x is complex by A2; ::_thesis: verum
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
let F be set ; ::_thesis: ( ( for X being set st X in F holds
X is ext-real-membered ) implies union F is ext-real-membered )
assume A1: for X being set st X in F holds
X is ext-real-membered ; ::_thesis: union F is ext-real-membered
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in union F implies x is ext-real )
assume x in union F ; ::_thesis: x is ext-real
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def_4;
X is ext-real-membered by A1, A3;
hence x is ext-real by A2; ::_thesis: verum
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
let F be set ; ::_thesis: ( ( for X being set st X in F holds
X is real-membered ) implies union F is real-membered )
assume A1: for X being set st X in F holds
X is real-membered ; ::_thesis: union F is real-membered
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in union F implies x is real )
assume x in union F ; ::_thesis: x is real
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def_4;
X is real-membered by A1, A3;
hence x is real by A2; ::_thesis: verum
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
let F be set ; ::_thesis: ( ( for X being set st X in F holds
X is rational-membered ) implies union F is rational-membered )
assume A1: for X being set st X in F holds
X is rational-membered ; ::_thesis: union F is rational-membered
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in union F implies x is rational )
assume x in union F ; ::_thesis: x is rational
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def_4;
X is rational-membered by A1, A3;
hence x is rational by A2; ::_thesis: verum
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
let F be set ; ::_thesis: ( ( for X being set st X in F holds
X is integer-membered ) implies union F is integer-membered )
assume A1: for X being set st X in F holds
X is integer-membered ; ::_thesis: union F is integer-membered
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in union F implies x is integer )
assume x in union F ; ::_thesis: x is integer
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def_4;
X is integer-membered by A1, A3;
hence x is integer by A2; ::_thesis: verum
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
let F be set ; ::_thesis: ( ( for X being set st X in F holds
X is natural-membered ) implies union F is natural-membered )
assume A1: for X being set st X in F holds
X is natural-membered ; ::_thesis: union F is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in union F implies x is natural )
assume x in union F ; ::_thesis: x is natural
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def_4;
X is natural-membered by A1, A3;
hence x is natural by A2; ::_thesis: verum
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{ P1[ set ] } :
ex X being complex-membered set st
for c being complex number holds
( c in X iff P1[c] )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in COMPLEX & P1[x] ) ) from XBOOLE_0:sch_1();
X is complex-membered
proof
let x be set ; :: according to MEMBERED:def_1 ::_thesis: ( x in X implies x is complex )
assume x in X ; ::_thesis: x is complex
then x in COMPLEX by A1;
hence x is complex ; ::_thesis: verum
end;
then reconsider X = X as complex-membered set ;
take X ; ::_thesis: for c being complex number holds
( c in X iff P1[c] )
let c be complex number ; ::_thesis: ( c in X iff P1[c] )
c in COMPLEX by XCMPLX_0:def_2;
hence ( c in X iff P1[c] ) by A1; ::_thesis: verum
end;
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] )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in ExtREAL & P1[x] ) ) from XBOOLE_0:sch_1();
X is ext-real-membered
proof
let x be set ; :: according to MEMBERED:def_2 ::_thesis: ( x in X implies x is ext-real )
assume x in X ; ::_thesis: x is ext-real
then x in ExtREAL by A1;
hence x is ext-real ; ::_thesis: verum
end;
then reconsider X = X as ext-real-membered set ;
take X ; ::_thesis: for e being ext-real number holds
( e in X iff P1[e] )
let e be ext-real number ; ::_thesis: ( e in X iff P1[e] )
e in ExtREAL by XXREAL_0:def_1;
hence ( e in X iff P1[e] ) by A1; ::_thesis: verum
end;
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] )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in REAL & P1[x] ) ) from XBOOLE_0:sch_1();
X is real-membered
proof
let x be set ; :: according to MEMBERED:def_3 ::_thesis: ( x in X implies x is real )
assume x in X ; ::_thesis: x is real
then x in REAL by A1;
hence x is real ; ::_thesis: verum
end;
then reconsider X = X as real-membered set ;
take X ; ::_thesis: for r being real number holds
( r in X iff P1[r] )
let r be real number ; ::_thesis: ( r in X iff P1[r] )
r in REAL by XREAL_0:def_1;
hence ( r in X iff P1[r] ) by A1; ::_thesis: verum
end;
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] )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in RAT & P1[x] ) ) from XBOOLE_0:sch_1();
X is rational-membered
proof
let x be set ; :: according to MEMBERED:def_4 ::_thesis: ( x in X implies x is rational )
assume x in X ; ::_thesis: x is rational
then x in RAT by A1;
hence x is rational ; ::_thesis: verum
end;
then reconsider X = X as rational-membered set ;
take X ; ::_thesis: for w being rational number holds
( w in X iff P1[w] )
let w be rational number ; ::_thesis: ( w in X iff P1[w] )
w in RAT by RAT_1:def_2;
hence ( w in X iff P1[w] ) by A1; ::_thesis: verum
end;
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] )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in INT & P1[x] ) ) from XBOOLE_0:sch_1();
X is integer-membered
proof
let x be set ; :: according to MEMBERED:def_5 ::_thesis: ( x in X implies x is integer )
assume x in X ; ::_thesis: x is integer
then x in INT by A1;
hence x is integer ; ::_thesis: verum
end;
then reconsider X = X as integer-membered set ;
take X ; ::_thesis: for i being integer number holds
( i in X iff P1[i] )
let i be integer number ; ::_thesis: ( i in X iff P1[i] )
i in INT by INT_1:def_2;
hence ( i in X iff P1[i] ) by A1; ::_thesis: verum
end;
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] )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in NAT & P1[x] ) ) from XBOOLE_0:sch_1();
X is natural-membered
proof
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in X implies x is natural )
assume x in X ; ::_thesis: x is natural
then x in NAT by A1;
hence x is natural ; ::_thesis: verum
end;
then reconsider X = X as natural-membered set ;
take X ; ::_thesis: for n being Nat holds
( n in X iff P1[n] )
let n be Nat; ::_thesis: ( n in X iff P1[n] )
n in NAT by ORDINAL1:def_12;
hence ( n in X iff P1[n] ) by A1; ::_thesis: verum
end;
registration
cluster non empty natural-membered for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is natural-membered )
proof
set X = the non empty natural-membered set ;
take the non empty natural-membered set ; ::_thesis: ( not the non empty natural-membered set is empty & the non empty natural-membered set is natural-membered )
thus ( not the non empty natural-membered set is empty & the non empty natural-membered set is natural-membered ) ; ::_thesis: verum
end;
end;
registration
cluster -> natural-membered for Element of NAT ;
coherence
for b1 being Element of NAT holds b1 is natural-membered
proof
let n be Element of NAT ; ::_thesis: n is natural-membered
let x be set ; :: according to MEMBERED:def_6 ::_thesis: ( x in n implies x is natural )
n c= omega by ORDINAL1:def_2;
hence ( x in n implies x is natural ) ; ::_thesis: verum
end;
end;
theorem :: MEMBERED:37
for X, Y being real-membered set st X <> {} & Y <> {} & ( for a, b being real number st a in X & b in Y holds
a <= b ) holds
ex d being real number st
( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) )
proof
let X, Y be real-membered set ; ::_thesis: ( X <> {} & Y <> {} & ( for a, b being real number st a in X & b in Y holds
a <= b ) implies ex d being real number st
( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) ) )
set x = the Element of X;
reconsider a = the Element of X as real number ;
set y = the Element of Y;
reconsider b = the Element of Y as real number ;
assume ( X <> {} & Y <> {} ) ; ::_thesis: ( ex a, b being real number st
( a in X & b in Y & not a <= b ) or ex d being real number st
( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) ) )
then A1: ( a in X & b in Y ) ;
A2: ( X c= REAL & Y c= REAL ) by Th3;
assume for a, b being real number st a in X & b in Y holds
a <= b ; ::_thesis: ex d being real number st
( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) )
then consider d being real number such that
A3: for a, b being real number st a in X & b in Y holds
( a <= d & d <= b ) by A2, AXIOMS:1;
reconsider d = d as real number ;
take d ; ::_thesis: ( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) )
thus ( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) ) by A1, A3; ::_thesis: verum
end;
definition
let X be set ;
attrX is add-closed means :: MEMBERED:def 25
for x, y being complex number st x in X & y in X holds
x + y in X;
end;
:: deftheorem defines add-closed MEMBERED:def_25_:_
for X being set holds
( X is add-closed iff for x, y being complex number st x in X & y in X holds
x + y in X );
registration
cluster empty -> add-closed for set ;
coherence
for b1 being set st b1 is empty holds
b1 is add-closed
proof
let X be set ; ::_thesis: ( X is empty implies X is add-closed )
assume A1: X is empty ; ::_thesis: X is add-closed
let x be complex number ; :: according to MEMBERED:def_25 ::_thesis: for y being complex number st x in X & y in X holds
x + y in X
thus for y being complex number st x in X & y in X holds
x + y in X by A1; ::_thesis: verum
end;
cluster COMPLEX -> add-closed ;
coherence
COMPLEX is add-closed
proof
let x be complex number ; :: according to MEMBERED:def_25 ::_thesis: for y being complex number st x in COMPLEX & y in COMPLEX holds
x + y in COMPLEX
thus for y being complex number st x in COMPLEX & y in COMPLEX holds
x + y in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
cluster REAL -> add-closed ;
coherence
REAL is add-closed
proof
let x be complex number ; :: according to MEMBERED:def_25 ::_thesis: for y being complex number st x in REAL & y in REAL holds
x + y in REAL
thus for y being complex number st x in REAL & y in REAL holds
x + y in REAL by XREAL_0:def_1; ::_thesis: verum
end;
cluster RAT -> add-closed ;
coherence
RAT is add-closed
proof
let x be complex number ; :: according to MEMBERED:def_25 ::_thesis: for y being complex number st x in RAT & y in RAT holds
x + y in RAT
thus for y being complex number st x in RAT & y in RAT holds
x + y in RAT by RAT_1:def_2; ::_thesis: verum
end;
cluster INT -> add-closed ;
coherence
INT is add-closed
proof
let x be complex number ; :: according to MEMBERED:def_25 ::_thesis: for y being complex number st x in INT & y in INT holds
x + y in INT
thus for y being complex number st x in INT & y in INT holds
x + y in INT by INT_1:def_2; ::_thesis: verum
end;
cluster NAT -> add-closed ;
coherence
NAT is add-closed
proof
let x be complex number ; :: according to MEMBERED:def_25 ::_thesis: for y being complex number st x in NAT & y in NAT holds
x + y in NAT
thus for y being complex number st x in NAT & y in NAT holds
x + y in NAT by ORDINAL1:def_12; ::_thesis: verum
end;
cluster non empty natural-membered add-closed for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is add-closed & b1 is natural-membered )
proof
take NAT ; ::_thesis: ( not NAT is empty & NAT is add-closed & NAT is natural-membered )
thus ( not NAT is empty & NAT is add-closed & NAT is natural-membered ) ; ::_thesis: verum
end;
end;