MEMBERED

:: On the Sets Inhabited by Numbers
::  by Andrzej Trybulec
::
:: Received August 23, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, ORDINAL1, NUMBERS,
      XBOOLE_0, SUBSET_1, TARSKI, SETFAM_1, MEMBERED, IDEAL_1, ARYTM_3, NAT_1,
      CARD_1, REAL_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, NAT_1;
 constructors ENUMSET1, SETFAM_1, XCMPLX_0, XXREAL_0, RAT_1, NUMBERS, NAT_1;
 registrations XREAL_0, INT_1, RAT_1, ORDINAL1, XCMPLX_0, NAT_1, XBOOLE_0;
 requirements BOOLE, SUBSET;
 definitions XCMPLX_0, XREAL_0, INT_1, TARSKI, RAT_1, XBOOLE_0, XXREAL_0;
 equalities XBOOLE_0;
 expansions XCMPLX_0, XREAL_0, INT_1, TARSKI, RAT_1, XBOOLE_0, XXREAL_0;
 theorems INT_1, XBOOLE_0, XREAL_0, XCMPLX_0, RAT_1, SUBSET_1, ORDINAL1,
      TARSKI, ENUMSET1, XBOOLE_1, SETFAM_1, NUMBERS, XXREAL_0, AXIOMS;
 schemes XBOOLE_0;

begin

reserve x for object, X, F for set;

definition
  let X be set;
  attr X is complex-membered means
  :Def1:
  x in X implies x is complex;
  attr X is ext-real-membered means
  :Def2:
  x in X implies x is ext-real;
  attr X is real-membered means
  :Def3:
  x in X implies x is real;
  attr X is rational-membered means
  :Def4:
  x in X implies x is rational;
  attr X is integer-membered means
  :Def5:
  x in X implies x is integer;
  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 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 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 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 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 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 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
  for X being non empty complex-membered set ex c st c in X
proof
  let X be non empty complex-membered set;
  ex x being object st x in X by XBOOLE_0:def 1;
  hence thesis;
end;

theorem
  for X being non empty ext-real-membered set ex e st e in X
proof
  let X be non empty ext-real-membered set;
  ex x being object st x in X by XBOOLE_0:def 1;
  hence thesis;
end;

theorem
  for X being non empty real-membered set ex r st r in X
proof
  let X be non empty real-membered set;
  ex x being object st x in X by XBOOLE_0:def 1;
  hence thesis;
end;

theorem
  for X being non empty rational-membered set ex w st w in X
proof
  let X be non empty rational-membered set;
  ex x being object st x in X by XBOOLE_0:def 1;
  hence thesis;
end;

theorem
  for X being non empty integer-membered set ex i st i in X
proof
  let X be non empty integer-membered set;
  ex x being object st x in X by XBOOLE_0:def 1;
  hence thesis;
end;

theorem
  for X being non empty natural-membered set ex n st n in X
proof
  let X be non empty natural-membered set;
  ex x being object st x in X by XBOOLE_0:def 1;
  hence thesis;
end;

theorem
  for X being 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
  for X being 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
  for X being 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
  for X being 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
  for X being 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
  for X being 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 Th19:
  for Y being complex-membered set st X c= Y holds X is complex-membered;

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

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

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

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

theorem Th24:
  for Y being 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;
  redefine pred X c= Y means  :: redefines c= (TARSKI, definition)

  c in X implies c in Y;
  compatibility;
end;

definition
  let X be ext-real-membered set, Y be set;
  redefine pred X c= Y means  :: redefines c= (TARSKI, definition)

  e in X implies e in Y;
  compatibility;
end;

definition
  let X be real-membered set, Y be set;
  redefine pred X c= Y means  :: redefines c= (MEMBERED, redefinition) → c= (TARSKI, definition)

  r in X implies r in Y;
  compatibility;
end;

definition
  let X be rational-membered set, Y be set;
  redefine pred X c= Y means  :: redefines c= (MEMBERED, redefinition) → c= (MEMBERED, redefinition) → c= (TARSKI, definition)

  w in X implies w in Y;
  compatibility;
end;

definition
  let X be integer-membered set, Y be set;
  redefine pred X c= Y means  :: redefines c= (MEMBERED, redefinition) → c= (MEMBERED, redefinition) → c= (MEMBERED, redefinition) → c= (TARSKI, definition)

  i in X implies i in Y;
  compatibility;
end;

definition
  let X be natural-membered set, Y be set;
  redefine pred X c= Y means  :: redefines c= (MEMBERED, redefinition) → c= (MEMBERED, redefinition) → c= (MEMBERED, redefinition) → c= (MEMBERED, redefinition) → c= (TARSKI, definition)

  n in X implies n in Y;
  compatibility;
end;

definition
  let X,Y be complex-membered set;
  redefine pred X = Y means  :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  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;
  redefine pred X = Y means  :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  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;
  redefine pred X = Y means  :: redefines = (MEMBERED, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  r in X iff r in Y;
  compatibility;
end;

definition
  let X,Y be rational-membered set;
  redefine pred X = Y means  :: redefines = (MEMBERED, redefinition) → = (MEMBERED, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  w in X iff w in Y;
  compatibility;
end;

definition
  let X,Y be integer-membered set;
  redefine pred X = Y means  :: redefines = (MEMBERED, redefinition) → = (MEMBERED, redefinition) → = (MEMBERED, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  i in X iff i in Y;
  compatibility;
end;

definition
  let X,Y be natural-membered set;
  redefine pred X = Y means  :: redefines = (MEMBERED, redefinition) → = (MEMBERED, redefinition) → = (MEMBERED, redefinition) → = (MEMBERED, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  n in X iff n in Y;
  compatibility;
end;

definition
  let X,Y be complex-membered set;
  redefine pred X misses Y means  :: redefines misses (XBOOLE_0, definition)
  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 being 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;
  redefine pred X misses Y means  :: redefines misses (XBOOLE_0, definition)
  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 being 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;
  redefine pred X misses Y means  :: redefines misses (MEMBERED, redefinition) → misses (XBOOLE_0, definition)
  not ex r st r in X & r in Y;
  compatibility;
end;

definition
  let X,Y be rational-membered set;
  redefine pred X misses Y means  :: redefines misses (MEMBERED, redefinition) → misses (MEMBERED, redefinition) → misses (XBOOLE_0, definition)
  not ex w st w in X & w in Y;
  compatibility;
end;

definition
  let X,Y be integer-membered set;
  redefine pred X misses Y means  :: redefines misses (MEMBERED, redefinition) → misses (MEMBERED, redefinition) → misses (MEMBERED, redefinition) → misses (XBOOLE_0, definition)
  not ex i st i in X & i in Y;
  compatibility;
end;

definition
  let X,Y be natural-membered set;
  redefine pred X misses Y means  :: redefines misses (MEMBERED, redefinition) → misses (MEMBERED, redefinition) → misses (MEMBERED, redefinition) → misses (MEMBERED, redefinition) → misses (XBOOLE_0, definition)
  not ex n st n in X & n in Y;
  compatibility;
end;

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

theorem
  for X st X in F & X is ext-real-membered holds meet F is
  ext-real-membered by Th20,SETFAM_1:3;

theorem
  for X st X in F & X is real-membered holds meet F is real-membered by Th21,
SETFAM_1:3;

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

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

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

scheme
  CMSeparation {P[object]}:
  ex X being complex-membered set st for c holds c in X
  iff P[c] proof
  consider X being set such that
A1: for x being 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
  EMSeparation {P[object]}:
   ex X being ext-real-membered set st for e holds e in
  X iff P[e] proof
  consider X being set such that
A1: for x being 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
  RMSeparation {P[object]}:
ex X being real-membered set st for r holds r in X
  iff P[r] proof
  consider X being set such that
A1: for x being 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
  WMSeparation {P[object]}:
 ex X being rational-membered set st for w holds w in
  X iff P[w] proof
  consider X being set such that
A1: for x being 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
  IMSeparation {P[object]}:
ex X being integer-membered set st for i holds i in X
  iff P[i] proof
  consider X being set such that
A1: for x being 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
  NMSeparation {P[object]}:
 ex X being natural-membered set st for n holds n in X
  iff P[n] proof
  consider X being set such that
A1: for x being 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;

:: From REAL_2, AG, 19.12.2008

reserve a,b,d for Real;

theorem
  for X,Y being 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 being Real such that
A3: for a,b being 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;

:: Added, AK, 2010.04.23

definition
  let X be set;
  attr X is add-closed means
  for x, y being 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;