membered.miz



    begin

    reserve x for object,

X,F for set;

    definition

      let X be set;

      :: MEMBERED:def1

      attr X is complex-membered means

      : Def1: x in X implies x is complex;

      :: MEMBERED:def2

      attr X is ext-real-membered means

      : Def2: x in X implies x is ext-real;

      :: MEMBERED:def3

      attr X is real-membered means

      : Def3: x in X implies x is real;

      :: MEMBERED:def4

      attr X is rational-membered means

      : Def4: x in X implies x is rational;

      :: MEMBERED:def5

      attr X is integer-membered means

      : Def5: x in X implies x is integer;

      :: MEMBERED:def6

      attr X is natural-membered means

      : Def6: x in X implies x is natural;

    end

    registration

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

      coherence

      proof

        let X;

        assume

         A1: X is natural-membered;

        let x;

        assume x in X;

        then x is natural by A1;

        then x in omega by ORDINAL1:def 12;

        hence x in INT by NUMBERS: 17;

      end;

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

      coherence

      proof

        let X;

        assume

         A2: X is integer-membered;

        let x;

        assume x in X;

        then x is integer by A2;

        then x in INT ;

        hence x in RAT by NUMBERS: 14;

      end;

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

      coherence

      proof

        let X;

        assume

         A3: X is rational-membered;

        let x;

        assume x in X;

        then x is rational by A3;

        then x in RAT ;

        hence x in REAL by NUMBERS: 12;

      end;

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

      coherence

      proof

        let X;

        assume

         A4: X is real-membered;

        let x;

        assume x in X;

        then x is real by A4;

        then x in REAL ;

        hence x in ExtREAL by NUMBERS: 31;

      end;

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

      coherence

      proof

        let X;

        assume

         A5: X is real-membered;

        let x;

        assume x in X;

        then x is real by A5;

        then x in REAL ;

        hence x in COMPLEX by NUMBERS: 11;

      end;

    end

    registration

      cluster non empty natural-membered for set;

      existence

      proof

        take { 0 };

        thus { 0 } is non empty;

        let x;

        assume x in { 0 };

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      cluster COMPLEX -> complex-membered;

      coherence ;

      cluster ExtREAL -> ext-real-membered;

      coherence

      proof

        let x;

        thus thesis;

      end;

      cluster REAL -> real-membered;

      coherence ;

      cluster RAT -> rational-membered;

      coherence

      proof

        let x;

        thus thesis;

      end;

      cluster INT -> integer-membered;

      coherence ;

      cluster NAT -> natural-membered;

      coherence ;

    end

    theorem :: MEMBERED:1

    

     Th1: X is complex-membered implies X c= COMPLEX

    proof

      assume

       A1: X is complex-membered;

      let x be object;

      assume x in X;

      then x is complex by A1;

      hence thesis;

    end;

    theorem :: MEMBERED:2

    

     Th2: X is ext-real-membered implies X c= ExtREAL

    proof

      assume

       A1: X is ext-real-membered;

      let x be object;

      assume x in X;

      then x is ext-real by A1;

      hence thesis;

    end;

    theorem :: MEMBERED:3

    

     Th3: X is real-membered implies X c= REAL

    proof

      assume

       A1: X is real-membered;

      let x be object;

      assume x in X;

      then x is real by A1;

      hence thesis;

    end;

    theorem :: MEMBERED:4

    

     Th4: X is rational-membered implies X c= RAT

    proof

      assume

       A1: X is rational-membered;

      let x be object;

      assume x in X;

      then x is rational by A1;

      hence thesis;

    end;

    theorem :: MEMBERED:5

    

     Th5: X is integer-membered implies X c= INT

    proof

      assume

       A1: X is integer-membered;

      let x be object;

      assume x in X;

      then x is integer by A1;

      hence thesis;

    end;

    theorem :: MEMBERED:6

    

     Th6: X is natural-membered implies X c= NAT by ORDINAL1:def 12;

    registration

      let X be complex-membered set;

      cluster -> complex for Element of X;

      coherence

      proof

        let e be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose X is non empty;

          hence thesis by Def1;

        end;

      end;

    end

    registration

      let X be ext-real-membered set;

      cluster -> ext-real for Element of X;

      coherence

      proof

        let e be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose X is non empty;

          hence thesis by Def2;

        end;

      end;

    end

    registration

      let X be real-membered set;

      cluster -> real for Element of X;

      coherence

      proof

        let e be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose X is non empty;

          hence thesis by Def3;

        end;

      end;

    end

    registration

      let X be rational-membered set;

      cluster -> rational for Element of X;

      coherence

      proof

        let e be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose X is non empty;

          hence thesis by Def4;

        end;

      end;

    end

    registration

      let X be integer-membered set;

      cluster -> integer for Element of X;

      coherence

      proof

        let e be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose X is non empty;

          hence thesis by Def5;

        end;

      end;

    end

    registration

      let X be natural-membered set;

      cluster -> natural for Element of X;

      coherence

      proof

        let e be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis by SUBSET_1:def 1;

        end;

          suppose X is non empty;

          hence thesis by Def6;

        end;

      end;

    end

    reserve c,c1,c2,c3 for Complex,

e,e1,e2,e3 for ExtReal,

r,r1,r2,r3 for Real,

w,w1,w2,w3 for Rational,

i,i1,i2,i3 for Integer,

n,n1,n2,n3 for Nat;

    theorem :: MEMBERED:7

    for X be non empty complex-membered set holds ex c st c in X

    proof

      let X be non empty complex-membered set;

      ex x be object st x in X by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: MEMBERED:8

    for X be non empty ext-real-membered set holds ex e st e in X

    proof

      let X be non empty ext-real-membered set;

      ex x be object st x in X by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: MEMBERED:9

    for X be non empty real-membered set holds ex r st r in X

    proof

      let X be non empty real-membered set;

      ex x be object st x in X by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: MEMBERED:10

    for X be non empty rational-membered set holds ex w st w in X

    proof

      let X be non empty rational-membered set;

      ex x be object st x in X by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: MEMBERED:11

    for X be non empty integer-membered set holds ex i st i in X

    proof

      let X be non empty integer-membered set;

      ex x be object st x in X by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: MEMBERED:12

    for X be non empty natural-membered set holds ex n st n in X

    proof

      let X be non empty natural-membered set;

      ex x be object st x in X by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: MEMBERED:13

    for X be complex-membered set st for c holds c in X holds X = COMPLEX

    proof

      let X be complex-membered set such that

       A1: for c holds c in X;

      thus X c= COMPLEX by Th1;

      let e be object;

      assume e in COMPLEX ;

      hence thesis by A1;

    end;

    theorem :: MEMBERED:14

    for X be ext-real-membered set st for e holds e in X holds X = ExtREAL

    proof

      let X be ext-real-membered set such that

       A1: for e holds e in X;

      thus X c= ExtREAL by Th2;

      let e be object;

      assume e in ExtREAL ;

      hence thesis by A1;

    end;

    theorem :: MEMBERED:15

    for X be real-membered set st for r holds r in X holds X = REAL

    proof

      let X be real-membered set such that

       A1: for r holds r in X;

      thus X c= REAL by Th3;

      let e be object;

      assume e in REAL ;

      hence thesis by A1;

    end;

    theorem :: MEMBERED:16

    for X be rational-membered set st for w holds w in X holds X = RAT

    proof

      let X be rational-membered set such that

       A1: for w holds w in X;

      thus X c= RAT by Th4;

      let e be object;

      assume e in RAT ;

      hence thesis by A1;

    end;

    theorem :: MEMBERED:17

    for X be integer-membered set st for i holds i in X holds X = INT

    proof

      let X be integer-membered set such that

       A1: for i holds i in X;

      thus X c= INT by Th5;

      let e be object;

      assume e in INT ;

      hence thesis by A1;

    end;

    theorem :: MEMBERED:18

    for X be natural-membered set st for n holds n in X holds X = NAT

    proof

      let X be natural-membered set such that

       A1: for n holds n in X;

      thus X c= NAT by Th6;

      let e be object;

      assume e in NAT ;

      hence thesis by A1;

    end;

    theorem :: MEMBERED:19

    

     Th19: for Y be complex-membered set st X c= Y holds X is complex-membered;

    theorem :: MEMBERED:20

    

     Th20: for Y be ext-real-membered set st X c= Y holds X is ext-real-membered;

    theorem :: MEMBERED:21

    

     Th21: for Y be real-membered set st X c= Y holds X is real-membered;

    theorem :: MEMBERED:22

    

     Th22: for Y be rational-membered set st X c= Y holds X is rational-membered;

    theorem :: MEMBERED:23

    

     Th23: for Y be integer-membered set st X c= Y holds X is integer-membered;

    theorem :: MEMBERED:24

    

     Th24: for Y be natural-membered set st X c= Y holds X is natural-membered;

    registration

      cluster empty -> natural-membered for set;

      coherence ;

    end

    registration

      let c;

      cluster {c} -> complex-membered;

      coherence by TARSKI:def 1;

    end

    registration

      let e be ExtReal;

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

      coherence by TARSKI:def 1;

    end

    registration

      let r;

      cluster {r} -> real-membered;

      coherence by TARSKI:def 1;

    end

    registration

      let w;

      cluster {w} -> rational-membered;

      coherence by TARSKI:def 1;

    end

    registration

      let i;

      cluster {i} -> integer-membered;

      coherence by TARSKI:def 1;

    end

    registration

      let n;

      cluster {n} -> natural-membered;

      coherence by TARSKI:def 1;

    end

    registration

      let c1, c2;

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

      coherence by TARSKI:def 2;

    end

    registration

      let e1,e2 be ExtReal;

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

      coherence by TARSKI:def 2;

    end

    registration

      let r1, r2;

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

      coherence by TARSKI:def 2;

    end

    registration

      let w1, w2;

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

      coherence by TARSKI:def 2;

    end

    registration

      let i1, i2;

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

      coherence by TARSKI:def 2;

    end

    registration

      let n1, n2;

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

      coherence by TARSKI:def 2;

    end

    registration

      let c1, c2, c3;

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

      coherence by ENUMSET1:def 1;

    end

    registration

      let e1,e2,e3 be ExtReal;

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

      coherence by ENUMSET1:def 1;

    end

    registration

      let r1, r2, r3;

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

      coherence by ENUMSET1:def 1;

    end

    registration

      let w1, w2, w3;

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

      coherence by ENUMSET1:def 1;

    end

    registration

      let i1, i2, i3;

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

      coherence by ENUMSET1:def 1;

    end

    registration

      let n1, n2, n3;

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

      coherence by ENUMSET1:def 1;

    end

    registration

      let X be complex-membered set;

      cluster -> complex-membered for Subset of X;

      coherence ;

    end

    registration

      let X be ext-real-membered set;

      cluster -> ext-real-membered for Subset of X;

      coherence ;

    end

    registration

      let X be real-membered set;

      cluster -> real-membered for Subset of X;

      coherence ;

    end

    registration

      let X be rational-membered set;

      cluster -> rational-membered for Subset of X;

      coherence ;

    end

    registration

      let X be integer-membered set;

      cluster -> integer-membered for Subset of X;

      coherence ;

    end

    registration

      let X be natural-membered set;

      cluster -> natural-membered for Subset of X;

      coherence ;

    end

    registration

      let X,Y be complex-membered set;

      cluster (X \/ Y) -> complex-membered;

      coherence

      proof

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    registration

      let X,Y be ext-real-membered set;

      cluster (X \/ Y) -> ext-real-membered;

      coherence

      proof

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    registration

      let X,Y be real-membered set;

      cluster (X \/ Y) -> real-membered;

      coherence

      proof

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    registration

      let X,Y be rational-membered set;

      cluster (X \/ Y) -> rational-membered;

      coherence

      proof

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    registration

      let X,Y be integer-membered set;

      cluster (X \/ Y) -> integer-membered;

      coherence

      proof

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    registration

      let X,Y be natural-membered set;

      cluster (X \/ Y) -> natural-membered;

      coherence

      proof

        let x;

        assume x in (X \/ Y);

        then x in X or x in Y by XBOOLE_0:def 3;

        hence thesis;

      end;

    end

    registration

      let X be complex-membered set, Y be set;

      cluster (X /\ Y) -> complex-membered;

      coherence by Th19, XBOOLE_1: 17;

      cluster (Y /\ X) -> complex-membered;

      coherence ;

    end

    registration

      let X be ext-real-membered set, Y be set;

      cluster (X /\ Y) -> ext-real-membered;

      coherence by Th20, XBOOLE_1: 17;

      cluster (Y /\ X) -> ext-real-membered;

      coherence ;

    end

    registration

      let X be real-membered set, Y be set;

      cluster (X /\ Y) -> real-membered;

      coherence by Th21, XBOOLE_1: 17;

      cluster (Y /\ X) -> real-membered;

      coherence ;

    end

    registration

      let X be rational-membered set, Y be set;

      cluster (X /\ Y) -> rational-membered;

      coherence by Th22, XBOOLE_1: 17;

      cluster (Y /\ X) -> rational-membered;

      coherence ;

    end

    registration

      let X be integer-membered set, Y be set;

      cluster (X /\ Y) -> integer-membered;

      coherence by Th23, XBOOLE_1: 17;

      cluster (Y /\ X) -> integer-membered;

      coherence ;

    end

    registration

      let X be natural-membered set, Y be set;

      cluster (X /\ Y) -> natural-membered;

      coherence by Th24, XBOOLE_1: 17;

      cluster (Y /\ X) -> natural-membered;

      coherence ;

    end

    registration

      let X be complex-membered set, Y be set;

      cluster (X \ Y) -> complex-membered;

      coherence ;

    end

    registration

      let X be ext-real-membered set, Y be set;

      cluster (X \ Y) -> ext-real-membered;

      coherence ;

    end

    registration

      let X be real-membered set, Y be set;

      cluster (X \ Y) -> real-membered;

      coherence ;

    end

    registration

      let X be rational-membered set, Y be set;

      cluster (X \ Y) -> rational-membered;

      coherence ;

    end

    registration

      let X be integer-membered set, Y be set;

      cluster (X \ Y) -> integer-membered;

      coherence ;

    end

    registration

      let X be natural-membered set, Y be set;

      cluster (X \ Y) -> natural-membered;

      coherence ;

    end

    registration

      let X,Y be complex-membered set;

      cluster (X \+\ Y) -> complex-membered;

      coherence ;

    end

    registration

      let X,Y be ext-real-membered set;

      cluster (X \+\ Y) -> ext-real-membered;

      coherence ;

    end

    registration

      let X,Y be real-membered set;

      cluster (X \+\ Y) -> real-membered;

      coherence ;

    end

    registration

      let X,Y be rational-membered set;

      cluster (X \+\ Y) -> rational-membered;

      coherence ;

    end

    registration

      let X,Y be integer-membered set;

      cluster (X \+\ Y) -> integer-membered;

      coherence ;

    end

    registration

      let X,Y be natural-membered set;

      cluster (X \+\ Y) -> natural-membered;

      coherence ;

    end

    definition

      let X be complex-membered set, Y be set;

      :: original: c=

      redefine

      :: MEMBERED:def7

      pred X c= Y means c in X implies c in Y;

      compatibility ;

    end

    definition

      let X be ext-real-membered set, Y be set;

      :: original: c=

      redefine

      :: MEMBERED:def8

      pred X c= Y means e in X implies e in Y;

      compatibility ;

    end

    definition

      let X be real-membered set, Y be set;

      :: original: c=

      redefine

      :: MEMBERED:def9

      pred X c= Y means r in X implies r in Y;

      compatibility ;

    end

    definition

      let X be rational-membered set, Y be set;

      :: original: c=

      redefine

      :: MEMBERED:def10

      pred X c= Y means w in X implies w in Y;

      compatibility ;

    end

    definition

      let X be integer-membered set, Y be set;

      :: original: c=

      redefine

      :: MEMBERED:def11

      pred X c= Y means i in X implies i in Y;

      compatibility ;

    end

    definition

      let X be natural-membered set, Y be set;

      :: original: c=

      redefine

      :: MEMBERED:def12

      pred X c= Y means n in X implies n in Y;

      compatibility ;

    end

    definition

      let X,Y be complex-membered set;

      :: original: =

      redefine

      :: MEMBERED:def13

      pred X = Y means c in X iff c in Y;

      compatibility

      proof

        thus X = Y implies for c holds c in X iff c in Y;

        assume c in X iff c in Y;

        hence X c= Y & Y c= X;

      end;

    end

    definition

      let X,Y be ext-real-membered set;

      :: original: =

      redefine

      :: MEMBERED:def14

      pred X = Y means e in X iff e in Y;

      compatibility

      proof

        thus X = Y implies for e holds e in X iff e in Y;

        assume e in X iff e in Y;

        then X c= Y & Y c= X;

        hence thesis;

      end;

    end

    definition

      let X,Y be real-membered set;

      :: original: =

      redefine

      :: MEMBERED:def15

      pred X = Y means r in X iff r in Y;

      compatibility ;

    end

    definition

      let X,Y be rational-membered set;

      :: original: =

      redefine

      :: MEMBERED:def16

      pred X = Y means w in X iff w in Y;

      compatibility ;

    end

    definition

      let X,Y be integer-membered set;

      :: original: =

      redefine

      :: MEMBERED:def17

      pred X = Y means i in X iff i in Y;

      compatibility ;

    end

    definition

      let X,Y be natural-membered set;

      :: original: =

      redefine

      :: MEMBERED:def18

      pred X = Y means n in X iff n in Y;

      compatibility ;

    end

    definition

      let X,Y be complex-membered set;

      :: original: misses

      redefine

      :: MEMBERED:def19

      pred X misses Y means not ex c st c in X & c in Y;

      compatibility

      proof

        thus X misses Y implies not ex c st c in X & c in Y by XBOOLE_0: 3;

        assume

         A1: not ex c st c in X & c in Y;

        assume X meets Y;

        then ex x be object st x in X & x in Y by XBOOLE_0: 3;

        hence thesis by A1;

      end;

    end

    definition

      let X,Y be ext-real-membered set;

      :: original: misses

      redefine

      :: MEMBERED:def20

      pred X misses Y means not ex e st e in X & e in Y;

      compatibility

      proof

        thus X misses Y implies not ex e st e in X & e in Y by XBOOLE_0: 3;

        assume

         A1: not ex e st e in X & e in Y;

        assume X meets Y;

        then ex x be object st x in X & x in Y by XBOOLE_0: 3;

        hence thesis by A1;

      end;

    end

    definition

      let X,Y be real-membered set;

      :: original: misses

      redefine

      :: MEMBERED:def21

      pred X misses Y means not ex r st r in X & r in Y;

      compatibility ;

    end

    definition

      let X,Y be rational-membered set;

      :: original: misses

      redefine

      :: MEMBERED:def22

      pred X misses Y means not ex w st w in X & w in Y;

      compatibility ;

    end

    definition

      let X,Y be integer-membered set;

      :: original: misses

      redefine

      :: MEMBERED:def23

      pred X misses Y means not ex i st i in X & i in Y;

      compatibility ;

    end

    definition

      let X,Y be natural-membered set;

      :: original: misses

      redefine

      :: MEMBERED:def24

      pred X misses Y means not ex n st n in X & n in Y;

      compatibility ;

    end

    theorem :: MEMBERED:25

    (for X st X in F holds X is complex-membered) implies ( union F) is complex-membered

    proof

      assume

       A1: for X st X in F holds X is complex-membered;

      let x;

      assume x in ( union F);

      then

      consider X such that

       A2: x in X and

       A3: X in F by TARSKI:def 4;

      X is complex-membered by A1, A3;

      hence thesis by A2;

    end;

    theorem :: MEMBERED:26

    (for X st X in F holds X is ext-real-membered) implies ( union F) is ext-real-membered

    proof

      assume

       A1: for X st X in F holds X is ext-real-membered;

      let x;

      assume x in ( union F);

      then

      consider X such that

       A2: x in X and

       A3: X in F by TARSKI:def 4;

      X is ext-real-membered by A1, A3;

      hence thesis by A2;

    end;

    theorem :: MEMBERED:27

    (for X st X in F holds X is real-membered) implies ( union F) is real-membered

    proof

      assume

       A1: for X st X in F holds X is real-membered;

      let x;

      assume x in ( union F);

      then

      consider X such that

       A2: x in X and

       A3: X in F by TARSKI:def 4;

      X is real-membered by A1, A3;

      hence thesis by A2;

    end;

    theorem :: MEMBERED:28

    (for X st X in F holds X is rational-membered) implies ( union F) is rational-membered

    proof

      assume

       A1: for X st X in F holds X is rational-membered;

      let x;

      assume x in ( union F);

      then

      consider X such that

       A2: x in X and

       A3: X in F by TARSKI:def 4;

      X is rational-membered by A1, A3;

      hence thesis by A2;

    end;

    theorem :: MEMBERED:29

    (for X st X in F holds X is integer-membered) implies ( union F) is integer-membered

    proof

      assume

       A1: for X st X in F holds X is integer-membered;

      let x;

      assume x in ( union F);

      then

      consider X such that

       A2: x in X and

       A3: X in F by TARSKI:def 4;

      X is integer-membered by A1, A3;

      hence thesis by A2;

    end;

    theorem :: MEMBERED:30

    (for X st X in F holds X is natural-membered) implies ( union F) is natural-membered

    proof

      assume

       A1: for X st X in F holds X is natural-membered;

      let x;

      assume x in ( union F);

      then

      consider X such that

       A2: x in X and

       A3: X in F by TARSKI:def 4;

      X is natural-membered by A1, A3;

      hence thesis by A2;

    end;

    theorem :: MEMBERED:31

    for X st X in F & X is complex-membered holds ( meet F) is complex-membered by Th19, SETFAM_1: 3;

    theorem :: MEMBERED:32

    for X 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 X st X in F & X is real-membered holds ( meet F) is real-membered by Th21, SETFAM_1: 3;

    theorem :: MEMBERED:34

    for X st X in F & X is rational-membered holds ( meet F) is rational-membered by Th22, SETFAM_1: 3;

    theorem :: MEMBERED:35

    for X st X in F & X is integer-membered holds ( meet F) is integer-membered by Th23, SETFAM_1: 3;

    theorem :: MEMBERED:36

    for X st X in F & X is natural-membered holds ( meet F) is natural-membered by Th24, SETFAM_1: 3;

    scheme :: MEMBERED:sch1

    CMSeparation { P[ object] } :

ex X be complex-membered set st for c holds c in X iff P[c];

      consider X be set such that

       A1: for x be object holds x in X iff x in COMPLEX & P[x] from XBOOLE_0:sch 1;

      X is complex-membered

      proof

        let x;

        assume x in X;

        then x in COMPLEX by A1;

        hence thesis;

      end;

      then

      reconsider X as complex-membered set;

      take X;

      let c;

      c in COMPLEX by XCMPLX_0:def 2;

      hence thesis by A1;

    end;

    scheme :: MEMBERED:sch2

    EMSeparation { P[ object] } :

ex X be ext-real-membered set st for e holds e in X iff P[e];

      consider X be set such that

       A1: for x be object holds x in X iff x in ExtREAL & P[x] from XBOOLE_0:sch 1;

      X is ext-real-membered

      proof

        let x;

        assume x in X;

        then x in ExtREAL by A1;

        hence thesis;

      end;

      then

      reconsider X as ext-real-membered set;

      take X;

      let e;

      e in ExtREAL by XXREAL_0:def 1;

      hence thesis by A1;

    end;

    scheme :: MEMBERED:sch3

    RMSeparation { P[ object] } :

ex X be real-membered set st for r holds r in X iff P[r];

      consider X be set such that

       A1: for x be object holds x in X iff x in REAL & P[x] from XBOOLE_0:sch 1;

      X is real-membered

      proof

        let x;

        assume x in X;

        then x in REAL by A1;

        hence thesis;

      end;

      then

      reconsider X as real-membered set;

      take X;

      let r;

      r in REAL by XREAL_0:def 1;

      hence thesis by A1;

    end;

    scheme :: MEMBERED:sch4

    WMSeparation { P[ object] } :

ex X be rational-membered set st for w holds w in X iff P[w];

      consider X be set such that

       A1: for x be object holds x in X iff x in RAT & P[x] from XBOOLE_0:sch 1;

      X is rational-membered

      proof

        let x;

        assume x in X;

        then x in RAT by A1;

        hence thesis;

      end;

      then

      reconsider X as rational-membered set;

      take X;

      let w;

      w in RAT by RAT_1:def 2;

      hence thesis by A1;

    end;

    scheme :: MEMBERED:sch5

    IMSeparation { P[ object] } :

ex X be integer-membered set st for i holds i in X iff P[i];

      consider X be set such that

       A1: for x be object holds x in X iff x in INT & P[x] from XBOOLE_0:sch 1;

      X is integer-membered

      proof

        let x;

        assume x in X;

        then x in INT by A1;

        hence thesis;

      end;

      then

      reconsider X as integer-membered set;

      take X;

      let i;

      i in INT by INT_1:def 2;

      hence thesis by A1;

    end;

    scheme :: MEMBERED:sch6

    NMSeparation { P[ object] } :

ex X be natural-membered set st for n holds n in X iff P[n];

      consider X be set such that

       A1: for x be object holds x in X iff x in NAT & P[x] from XBOOLE_0:sch 1;

      X is natural-membered

      proof

        let x;

        assume x in X;

        then x in NAT by A1;

        hence thesis;

      end;

      then

      reconsider X as natural-membered set;

      take X;

      let n;

      n in NAT by ORDINAL1:def 12;

      hence thesis by A1;

    end;

    registration

      cluster non empty natural-membered for set;

      existence

      proof

        set X = the non empty natural-membered set;

        take X;

        thus thesis;

      end;

    end

    reserve a,b,d for Real;

    theorem :: MEMBERED:37

    for X,Y be real-membered set st X <> {} & Y <> {} & for a, b st a in X & b in Y holds a <= b holds ex d st (for a st a in X holds a <= d) & for b st b in Y holds d <= b

    proof

      let X,Y be real-membered set;

      set x = the Element of X;

      reconsider a = x as Real;

      set y = the Element of Y;

      reconsider b = y as Real;

      assume X <> {} & Y <> {} ;

      then

       A1: a in X & b in Y;

      

       A2: X c= REAL & Y c= REAL by Th3;

      assume for a, b st a in X & b in Y holds a <= b;

      then

      consider d be Real such that

       A3: for a,b be Real st a in X & b in Y holds a <= d & d <= b by A2, AXIOMS: 1;

      reconsider d as Real;

      take d;

      thus thesis by A1, A3;

    end;

    definition

      let X be set;

      :: MEMBERED:def25

      attr X is add-closed means for x,y be Complex st x in X & y in X holds (x + y) in X;

    end

    registration

      cluster empty -> add-closed for set;

      coherence ;

      cluster COMPLEX -> add-closed;

      coherence by XCMPLX_0:def 2;

      cluster REAL -> add-closed;

      coherence by XREAL_0:def 1;

      cluster RAT -> add-closed;

      coherence by RAT_1:def 2;

      cluster INT -> add-closed;

      coherence by INT_1:def 2;

      cluster NAT -> add-closed;

      coherence by ORDINAL1:def 12;

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

      existence

      proof

        take NAT ;

        thus thesis;

      end;

    end