ZFMISC_1

:: Some Basic Properties of Sets
::  by Czes{\l}aw Byli\'nski
::
:: Received February 1, 1989
:: Copyright (c) 1990-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 XBOOLE_0, TARSKI, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ENUMSET1;
 constructors TARSKI, XBOOLE_0, ENUMSET1;
 registrations XBOOLE_0;
 requirements BOOLE;
 definitions TARSKI, XBOOLE_0;
 equalities TARSKI, XBOOLE_0;
 expansions TARSKI, XBOOLE_0;
 theorems TARSKI, XBOOLE_0, ENUMSET1, XBOOLE_1, XTUPLE_0, XREGULAR, TARSKI_A;
 schemes XBOOLE_0, XFAMILY;

begin

reserve u,v,x,x1,x2,y,y1,y2,z,p,a for object,
        A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set;

Lm1: {x} c= X iff x in X
proof
  x in {x} by TARSKI:def 1;
  hence {x} c= X implies x in X;
  assume
A1: x in X;
  let y;
  thus thesis by A1,TARSKI:def 1;
end;

Lm2: Y c= X & not x in Y implies Y c= X \ { x }
proof
  assume
A1: Y c= X & not x in Y;
  let y;
  assume y in Y;
  then y in X & not y in { x } by A1,TARSKI:def 1;
  hence thesis by XBOOLE_0:def 5;
end;

Lm3:
 Y c= { x } iff Y = {} or Y = { x }
proof
  thus Y c= { x } implies Y = {} or Y = { x }
  proof
    assume
A1: Y c= { x };
    x in Y or not x in Y;
    then { x } c= Y or Y c= { x } \ { x } by A1,Lm1,Lm2;
    then { x } = Y or Y c= {} by A1,XBOOLE_1:37;
    hence thesis by XBOOLE_1:3;
  end;
  thus thesis;
end;

definition
  let X;
  defpred IT[set] means $1 c= X;
  func bool X -> set means
  :Def1:
  Z in it iff Z c= X;
  existence
  proof
    consider M such that
A1: X in M & for X,Y holds X in M & Y c= X implies Y in M and
    for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z and
    for X holds X c= M implies X,M are_equipotent or X in M by TARSKI_A:1;
    consider IT being set such that
A2: Y in IT iff Y in M & IT[Y] from XFAMILY:sch 1;
    take IT;
    thus thesis by A2,A1;
  end;
  uniqueness
  proof
    thus for X1,X2 being set st (for x being set holds x in X1 iff IT[x]) & (
    for x being set holds x in X2 iff IT[x]) holds X1 = X2 from XFAMILY:sch 3;
  end;
end;

definition
  let X1,X2;
  defpred X[object] means
    ex x,y st x in X1 & y in X2 & $1 = [x,y];
  func [: X1,X2 :] -> set means
:Def2:
    z in it iff ex x,y st x in X1 & y in X2 & z = [x,y];
  existence
  proof
A1: X1 c= X1 \/ X2 by XBOOLE_1:7;
    consider X such that
A2: for z holds z in X iff z in bool(bool(X1 \/ X2)) & X[z] from
    XBOOLE_0:sch 1;
    take X;
    let z;
    thus z in X implies
     ex x,y st x in X1 & y in X2 & z = [x,y] by A2;
    given x,y such that
A3: x in X1 and
A4: y in X2 and
A5: z = [x,y];
    {x,y} c= X1 \/ X2
    proof
      let z;
      assume z in {x,y};
      then z = x or z = y by TARSKI:def 2;
      hence thesis by A3,A4,XBOOLE_0:def 3;
    end;
    then
A6: {x,y} in bool(X1 \/ X2) by Def1;
    {x} c= X1 \/ X2 by A1,A3,Lm1;
    then
A7: {x} in bool(X1 \/ X2) by Def1;
    {{x,y},{x}} c= bool(X1 \/ X2)
    by A7,A6,TARSKI:def 2;
    then {{x,y},{x}} in bool(bool(X1 \/ X2)) by Def1;
    hence thesis by A2,A3,A4,A5;
  end;
  uniqueness
  proof
    thus for X1,X2 being set
      st (for x holds x in X1 iff X[x]) & (for x holds x in X2 iff X[x])
      holds X1 = X2
     from XBOOLE_0:sch 3;
  end;
end;

definition
  let X1,X2,X3;
  func [: X1,X2,X3 :] -> set equals
  [:[:X1,X2:],X3:];
  coherence;
end;

definition
  let X1,X2,X3,X4;
  func [: X1,X2,X3,X4 :] -> set equals
  [:[:X1,X2,X3:],X4:];
  coherence;
end;

begin

::
::  Empty set.
::

theorem
  bool {} = { {} }
proof
  now
    let x;
    reconsider xx = x as set by TARSKI:1;
    xx c= {} iff x = {} by XBOOLE_1:3;
    hence x in bool {} iff x in { {} } by Def1,TARSKI:def 1;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  union {} = {}
proof
  now
    given x such that
A1: x in union {};
    ex X being set st x in X & X in {} by A1,TARSKI:def 4;
    hence contradiction;
  end;
  hence thesis by XBOOLE_0:7;
end;

::
::  Singleton and unordered pairs.
::

theorem Th3:
  {x} c= {y} implies x = y
proof
  x in { x } by TARSKI:def 1;
  then {x} = {y} implies x = y by TARSKI:def 1;
  hence thesis by Lm3;
end;

theorem Th4:
  {x} = {y1,y2} implies x = y1
proof
  assume { x } = { y1,y2 };
  then y1 in { x } by TARSKI:def 2;
  hence thesis by TARSKI:def 1;
end;

theorem
  {x} = {y1,y2} implies y1 = y2
proof
  assume
A1: { x } = { y1,y2 };
  then x = y1 by Th4;
  hence thesis by A1,Th4;
end;

theorem Th6:
  { x1,x2 } = { y1,y2 } implies x1 = y1 or x1 = y2
proof
  x1 in { x1,x2 } by TARSKI:def 2;
  hence thesis by TARSKI:def 2;
end;

theorem Th7:
  {x} c= {x,y}
proof
  let z;
  assume z in {x};
  then z=x by TARSKI:def 1;
  hence thesis by TARSKI:def 2;
end;

Lm4: {x} \/ X c= X implies x in X
proof
  assume
A1: {x} \/ X c= X;
  assume not x in X;
  then not x in {x} \/ X by A1;
  then not x in {x} by XBOOLE_0:def 3;
  hence thesis by TARSKI:def 1;
end;

theorem
  {x} \/ {y} = {x} implies x = y
proof
  assume {x} \/ {y} = {x};
  then y in {x} or x in {y} by Lm4;
  hence thesis by TARSKI:def 1;
end;

theorem
  {x} \/ {x,y} = {x,y}
proof
  x in {x,y} by TARSKI:def 2;
  hence thesis by Lm1,XBOOLE_1:12;
end;

Lm5: {x} misses X implies not x in X
proof
A1: x in {x} by TARSKI:def 1;
  assume {x} /\ X = {} & x in X;
  hence contradiction by A1,XBOOLE_0:def 4;
end;

theorem
  {x} misses {y} implies x <> y;

Lm6: not x in X implies {x} misses X
proof
  assume
A1: not x in X;
  thus {x} /\ X c= {}
  proof
    let y;
    assume y in {x} /\ X;
    then y in {x} & y in X by XBOOLE_0:def 4;
    hence thesis by A1,TARSKI:def 1;
  end;
  thus thesis;
end;

theorem Th11:
  x <> y implies {x} misses {y}
proof
  assume x <> y;
  then not x in {y} by TARSKI:def 1;
  hence thesis by Lm6;
end;

Lm7: X /\ {x} = {x} implies x in X
proof
  assume X /\ {x} = {x};
  then x in X /\ {x} by TARSKI:def 1;
  hence thesis by XBOOLE_0:def 4;
end;

theorem
  {x} /\ {y} = {x} implies x = y
proof
  assume {x} /\ {y} = {x};
  then x in {y} or y in {x} by Lm7;
  hence thesis by TARSKI:def 1;
end;

Lm8: x in X implies X /\ {x} = {x} by Lm1,XBOOLE_1:28;

theorem
  {x} /\ {x,y} = {x}
proof
  x in {x,y} by TARSKI:def 2;
  hence thesis by Lm1,XBOOLE_1:28;
end;

Lm9: {x} \ X = {x} iff not x in X by Lm5,Lm6,XBOOLE_1:83;

theorem
  {x} \ {y} = {x} iff x <> y
proof
  {x} \ {y} = {x} iff not x in {y} by Lm5,Lm6,XBOOLE_1:83;
  hence thesis by TARSKI:def 1;
end;

Lm10: {x} \ X = {} iff x in X by Lm1,XBOOLE_1:37;

theorem
  {x} \ {y} = {} implies x = y
proof
  assume {x} \ {y} = {};
  then x in {y} by Lm1,XBOOLE_1:37;
  hence thesis by TARSKI:def 1;
end;

theorem
  {x} \ {x,y} = {}
proof
  x in {x,y} by TARSKI:def 2;
  hence thesis by Lm1,XBOOLE_1:37;
end;

Lm11: {x,y} \ X = {x} iff not x in X & (y in X or x = y)
proof
  thus {x,y} \ X = {x} implies not x in X & (y in X or x = y)
  proof
    assume
A1: {x,y} \ X = {x};
    then x in {x,y} \ X by TARSKI:def 1;
    hence not x in X by XBOOLE_0:def 5;
A2: y in {x,y} by TARSKI:def 2;
    assume not y in X;
    then y in {x} by A1,A2,XBOOLE_0:def 5;
    hence thesis by TARSKI:def 1;
  end;
  assume
A3: ( not x in X)&( y in X or x=y);
  for z holds z in {x,y} \ X iff z=x
  proof
    let z;
    z in {x,y} \ X iff z in {x,y} & not z in X by XBOOLE_0:def 5;
    hence thesis by A3,TARSKI:def 2;
  end;
  hence thesis by TARSKI:def 1;
end;

theorem
  x <> y implies { x,y } \ { y } = { x }
proof
  assume x <> y;
  then
A1: not x in {y} by TARSKI:def 1;
  y in {y} by TARSKI:def 1;
  hence thesis by A1,Lm11;
end;

theorem
  {x} c= {y} implies x = y by Th3;

theorem
  {z} c= {x,y} implies z = x or z = y
proof
A1: z in {z} by TARSKI:def 1;
  assume {z} c= {x,y};
  then z in {x,y} by A1;
  hence thesis by TARSKI:def 2;
end;

theorem Th20:
  {x,y} c= {z} implies x = z
proof
A1: x in {x,y} by TARSKI:def 2;
  assume {x,y} c= {z};
  then x in {z} by A1;
  hence thesis by TARSKI:def 1;
end;

theorem
  {x,y} c= {z} implies {x,y} = {z}
proof
  assume {x,y} c= {z};
  then x=z & y=z by Th20;
  hence thesis by ENUMSET1:29;
end;

Lm12: X <> {x} & X <> {} implies ex y st y in X & y <> x
proof
  assume that
A1: X <> {x} and
A2: X <> {};
  per cases;
  suppose
A3: not x in X;
    consider y such that
A4: y in X by A2,XBOOLE_0:7;
    take y;
    thus thesis by A3,A4;
  end;
  suppose
A5: x in X;
    consider y such that
A6: y in X & not y in {x} or y in {x} & not y in X by A1,TARSKI:2;
    take y;
    thus thesis by A5,A6,TARSKI:def 1;
  end;
end;

Lm13: Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2}
proof
  thus Z c= {x1,x2} implies Z={} or Z={x1} or Z={x2} or Z={x1,x2}
  proof
    assume that
A1: Z c= {x1,x2} and
A2: Z <> {} and
A3: Z <> {x1} and
A4: Z <> {x2};
    now
      let z;
      thus z in Z implies z in {x1,x2} by A1;
A5:   now
        assume
A6:     not x1 in Z;
        consider y such that
A7:     y in Z and
A8:     y<>x2 by A2,A4,Lm12;
        y in {x1,x2} by A1,A7;
        hence contradiction by A6,A7,A8,TARSKI:def 2;
      end;
A9:   now
        assume
A10:    not x2 in Z;
        consider y such that
A11:    y in Z and
A12:    y<>x1 by A2,A3,Lm12;
        y in {x1,x2} by A1,A11;
        hence contradiction by A10,A11,A12,TARSKI:def 2;
      end;
      assume z in {x1,x2};
      hence z in Z by A5,A9,TARSKI:def 2;
    end;
    hence thesis by TARSKI:2;
  end;
  thus thesis by Th7;
end;

theorem
  {x1,x2} c= {y1,y2} implies x1 = y1 or x1 = y2
proof
  assume {x1,x2} c= {y1,y2};
  then {x1,x2}={} or {x1,x2}={y1} or {x1,x2}={y2} or {x1,x2}={y1,y2} by Lm13;
  hence thesis by Th4,Th6;
end;

theorem
  x <> y implies { x } \+\ { y } = { x,y }
proof
  assume
A1: x <> y;
  for z holds z in { x } \+\ { y } iff z=x or z=y
  proof
    let z;
A2: z in {y} iff z=y by TARSKI:def 1;
    z in {x} iff z=x by TARSKI:def 1;
    hence thesis by A1,A2,XBOOLE_0:1;
  end;
  hence thesis by TARSKI:def 2;
end;

theorem
  bool { x } = { {} , { x }}
proof
  now
    let y;
     reconsider yy = y as set by TARSKI:1;
    yy c= { x } iff y = {} or y = { x } by Lm3;
    hence y in bool { x } iff y in { {}, { x }} by Def1,TARSKI:def 2;
  end;
  hence thesis by TARSKI:2;
end;

Lm14: X in A implies X c= union A
by TARSKI:def 4;

registration let x be object;
 reduce union { x } to x;
 reducibility
  proof
   reconsider X = x as set by TARSKI:1;
A1: union { X } c= X
     proof
      let y;
       assume y in union { X };
        then ex Y being set st y in Y & Y in { X } by TARSKI:def 4;
      hence thesis by TARSKI:def 1;
     end;
    X in { X } by TARSKI:def 1;
    then X c= union { X } by Lm14;
   hence thesis by A1,XBOOLE_0:def 10;
  end;
end;

theorem
  union { x } = x;

Lm15: union { X,Y } = X \/ Y
proof
  x in union {X,Y} iff x in X or x in Y
  proof
    thus x in union {X,Y} implies x in X or x in Y
    proof
      assume x in union {X,Y};
      then ex Z st x in Z & Z in {X,Y} by TARSKI:def 4;
      hence thesis by TARSKI:def 2;
    end;
    X in {X,Y} & Y in {X,Y} by TARSKI:def 2;
    hence thesis by TARSKI:def 4;
  end;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  union {{x},{y}} = {x,y}
proof
  thus union {{x},{y}} = {x} \/ {y} by Lm15
    .= {x,y} by ENUMSET1:1;
end;

::
::  Ordered pairs.
::

Lm16: [x,y] in [:X,Y:] iff x in X & y in Y
proof
  thus [x,y] in [:X,Y:] implies x in X & y in Y
  proof
    assume [x,y] in [:X,Y:];
    then ex x1,y1 st x1 in X & y1 in Y & [x,y]=[x1,y1] by Def2;
    hence thesis by XTUPLE_0:1;
  end;
  thus thesis by Def2;
end;

::$CT

theorem
  [x,y] in [:{x1},{y1}:] iff x = x1 & y = y1
proof
  x=x1 & y=y1 iff x in {x1} & y in {y1} by TARSKI:def 1;
  hence thesis by Lm16;
end;

theorem Th28:
  [:{x},{y}:] = {[x,y]}
proof
  now
    let z;
    thus z in [:{x},{y}:] implies z in {[x,y]}
    proof
      assume z in [:{x},{y}:];
      then consider x1,y1 such that
A1:   x1 in {x} & y1 in {y} and
A2:   z=[x1,y1] by Def2;
      x1=x & y1=y by A1,TARSKI:def 1;
      hence thesis by A2,TARSKI:def 1;
    end;
    assume z in {[x,y]};
    then
A3: z=[x,y] by TARSKI:def 1;
    x in {x} & y in {y} by TARSKI:def 1;
    hence z in [:{x},{y}:] by A3,Lm16;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th29:
  [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]}
proof
  now
    let v;
A1: z in{y,z} by TARSKI:def 2;
    thus v in [:{x},{y,z}:] implies v in {[x,y],[x,z]}
    proof
      assume v in [:{x},{y,z}:];
      then consider x1,y1 such that
A2:   x1 in {x} and
A3:   y1 in {y,z} and
A4:   v=[x1,y1] by Def2;
A5:   y1=y or y1=z by A3,TARSKI:def 2;
      x1=x by A2,TARSKI:def 1;
      hence thesis by A4,A5,TARSKI:def 2;
    end;
    assume v in {[x,y],[x,z]};
    then
A6: v=[x,y] or v=[x,z] by TARSKI:def 2;
    x in{x} & y in{y,z} by TARSKI:def 1,def 2;
    hence v in [:{x},{y,z}:] by A6,A1,Lm16;
  end;
  hence [:{x},{y,z}:] = {[x,y],[x,z]} by TARSKI:2;
  now
    let v;
A7: z in{z} by TARSKI:def 1;
    thus v in [:{x,y},{z}:] implies v in {[x,z],[y,z]}
    proof
      assume v in [:{x,y},{z}:];
      then consider x1,y1 such that
A8:   x1 in {x,y} and
A9:   y1 in {z} and
A10:  v=[x1,y1] by Def2;
A11:  x1=x or x1=y by A8,TARSKI:def 2;
      y1=z by A9,TARSKI:def 1;
      hence thesis by A10,A11,TARSKI:def 2;
    end;
    assume v in {[x,z],[y,z]};
    then
A12: v=[x,z] or v=[y,z] by TARSKI:def 2;
    x in{x,y} & y in{x,y} by TARSKI:def 2;
    hence v in [:{x,y},{z}:] by A12,A7,Lm16;
  end;
  hence thesis by TARSKI:2;
end;

::
::  Singleton and unordered pairs included in a set.
::

theorem
  {x} c= X iff x in X by Lm1;

theorem Th31:
  {x1,x2} c= Z iff x1 in Z & x2 in Z
proof
  x1 in {x1,x2} & x2 in {x1,x2} by TARSKI:def 2;
  hence {x1,x2} c= Z implies x1 in Z & x2 in Z;
  assume
A1: x1 in Z & x2 in Z;
  let z;
  assume z in {x1,x2};
  hence thesis by A1,TARSKI:def 2;
end;

::
::  Set included in a singleton (or unordered pair).
::

theorem
  Y c= { x } iff Y = {} or Y = { x } by Lm3;

theorem
  Y c= X & not x in Y implies Y c= X \ { x } by Lm2;

theorem
  X <> {x} & X <> {} implies ex y st y in X & y <> x by Lm12;

theorem
  Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} by Lm13;

::
::   Sum of an unordered pair (or a singleton) and a set.
::

theorem Th36:
  {z} = X \/ Y implies X = {z} & Y = {z} or X = {} & Y = {z} or X
  = {z} & Y = {}
proof
  assume
A1: {z} = X \/ Y;
  X <> {} or Y <> {} by A1;
  hence thesis by A1,Lm3,XBOOLE_1:7;
end;

theorem
  {z} = X \/ Y & X <> Y implies X = {} or Y = {}
proof
  assume {z} = X \/ Y;
  then X={z} & Y={z} or X={} & Y={z} or X={z} & Y={} by Th36;
  hence thesis;
end;

theorem
  {x} \/ X c= X implies x in X by Lm4;

theorem
  x in X implies {x} \/ X = X by Lm1,XBOOLE_1:12;

theorem
  {x,y} \/ Z c= Z implies x in Z
proof
  assume
A1: {x,y} \/ Z c= Z;
  assume not x in Z;
  then not x in {x,y} \/ Z by A1;
  then not x in {x,y} by XBOOLE_0:def 3;
  hence thesis by TARSKI:def 2;
end;

theorem
  x in Z & y in Z implies {x,y} \/ Z = Z by Th31,XBOOLE_1:12;

theorem
  {x} \/ X <> {};

theorem
  {x,y} \/ X <> {};

::
::  Intersection of an unordered pair (or a singleton) and a set.
::

theorem
  X /\ {x} = {x} implies x in X by Lm7;

theorem
  x in X implies X /\ {x} = {x} by Lm1,XBOOLE_1:28;

theorem
  x in Z & y in Z implies {x,y} /\ Z = {x,y} by Th31,XBOOLE_1:28;

theorem
  {x} misses X implies not x in X by Lm5;

theorem Th48:
  {x,y} misses Z implies not x in Z
proof
A1: x in {x,y} by TARSKI:def 2;
  assume {x,y} /\ Z = {} & x in Z;
  hence contradiction by A1,XBOOLE_0:def 4;
end;

theorem
  not x in X implies {x} misses X by Lm6;

theorem Th50:
  not x in Z & not y in Z implies {x,y} misses Z
proof
  assume
A1: ( not x in Z)& not y in Z;
  assume {x,y} meets Z;
  then consider z such that
A2: z in {x,y} /\ Z by XBOOLE_0:4;
  z in {x,y} & z in Z by A2,XBOOLE_0:def 4;
  hence contradiction by A1,TARSKI:def 2;
end;

theorem
  {x} misses X or {x} /\ X = {x} by Lm6,Lm8;

theorem
  {x,y} /\ X = {x} implies not y in X or x = y
proof
A1: y in {x,y} by TARSKI:def 2;
  assume {x,y} /\ X = {x} & y in X;
  then y in {x} by A1,XBOOLE_0:def 4;
  hence thesis by TARSKI:def 1;
end;

theorem
  x in X & (not y in X or x = y) implies {x,y} /\ X = {x}
proof
  assume
A1: x in X &( not y in X or x=y);
  for z holds z in {x,y} /\ X iff z=x
  proof
    let z be object;
    z in {x,y} /\ X iff z in {x,y} & z in X by XBOOLE_0:def 4;
    hence thesis by A1,TARSKI:def 2;
  end;
  hence thesis by TARSKI:def 1;
end;

theorem
  {x,y} /\ X = {x,y} implies x in X
proof
  assume {x,y} /\ X = {x,y};
  then x in {x,y} /\ X & y in {x,y} /\ X or x in X /\ {x,y} & y in X /\ {x,y}
  by TARSKI:def 2;
  hence thesis by XBOOLE_0:def 4;
end;

::
::   Difference of an unordered pair (or a singleton) and a set.
::

theorem Th55:
  z in X \ {x} iff z in X & z <> x
proof
  z in X \ {x} iff z in X & not z in {x} by XBOOLE_0:def 5;
  hence thesis by TARSKI:def 1;
end;

theorem Th56:
  X \ {x} = X iff not x in X
proof
  X \ {x} = X iff X misses {x} by XBOOLE_1:83;
  hence thesis by Lm5,Lm6;
end;

theorem
  X \ {x} = {} implies X = {} or X = {x}
proof
  assume X \ {x} = {};
  then X c= {x} by XBOOLE_1:37;
  hence thesis by Lm3;
end;

theorem
  {x} \ X = {x} iff not x in X by Lm5,Lm6,XBOOLE_1:83;

theorem
  {x} \ X = {} iff x in X by Lm1,XBOOLE_1:37;

theorem
  {x} \ X = {} or {x} \ X = {x} by Lm9,Lm10;

theorem
  {x,y} \ X = {x} iff not x in X & (y in X or x = y) by Lm11;

theorem
  {x,y} \ X = {x,y} iff not x in X & not y in X by Th48,Th50,XBOOLE_1:83;

theorem Th63:
  {x,y} \ X = {} iff x in X & y in X
proof
  {x,y} \ X = {} iff {x,y} c= X by XBOOLE_1:37;
  hence thesis by Th31;
end;

theorem
  {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x ,y}
proof
  assume that
A1: {x,y} \ X <> {} and
A2: {x,y} \ X <> {x} and
A3: {x,y} \ X <> {y};
A4: not x in X & x<>y or y in X by A3,Lm11;
  x in X or not y in X & x<>y by A2,Lm11;
  hence thesis by A1,A4,Th50,Th63,XBOOLE_1:83;
end;

theorem
  X \ {x,y} = {} iff X = {} or X = {x} or X = {y} or X = {x,y}
proof
  X \ {x,y} = {} iff X c= {x,y} by XBOOLE_1:37;
  hence thesis by Lm13;
end;

::
::  Power Set.
::

theorem
  A c= B implies bool A c= bool B
proof
  assume
A1: A c= B;
  let x;
   reconsider xx=x as set by TARSKI:1;
  assume x in bool A;
  then xx c= A by Def1;
  then xx c= B by A1;
  hence thesis by Def1;
end;

theorem
  { A } c= bool A
proof
  A in bool A by Def1;
  hence thesis by Lm1;
end;

theorem
  bool A \/ bool B c= bool (A \/ B)
proof
  let x;
   reconsider xx=x as set by TARSKI:1;
  assume x in bool A \/ bool B;
  then x in bool A or x in bool B by XBOOLE_0:def 3;
  then
A1: xx c= A or xx c= B by Def1;
  A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
  then xx c= A \/ B by A1;
  hence thesis by Def1;
end;

theorem
  bool A \/ bool B = bool (A \/ B) implies A,B are_c=-comparable
proof
  assume
A1: bool A \/ bool B = bool (A \/ B);
  A \/ B in bool (A \/ B) by Def1;
  then A \/ B in bool A or A \/ B in bool B by A1,XBOOLE_0:def 3;
  then
A2: A \/ B c= A or A \/ B c= B by Def1;
  A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
  hence A c= B or B c= A by A2;
end;

theorem
  bool (A /\ B) = bool A /\ bool B
proof
  now
    let x;
     reconsider xx=x as set by TARSKI:1;
    A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
    then xx c= A & xx c= B iff xx c= A /\ B by XBOOLE_1:19;
    then x in bool A & x in bool B iff x in bool (A /\ B) by Def1;
    hence x in bool (A /\ B) iff x in bool A /\ bool B by XBOOLE_0:def 4;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  bool (A \ B) c= { {} } \/ (bool A \ bool B)
proof
  let x;
   reconsider xx=x as set by TARSKI:1;
  assume x in bool (A \ B);
  then
A1: xx c= A \ B by Def1;
  then xx misses B by XBOOLE_1:63,79;
  then A \ B c= A & xx /\ B = {} by XBOOLE_1:36;
  then x = {} or xx c= A & not xx c= B by A1,XBOOLE_1:28;
  then x in { {} } or x in bool A & not x in bool B by Def1,TARSKI:def 1;
  then x in { {} } or x in bool A \ bool B by XBOOLE_0:def 5;
  hence thesis by XBOOLE_0:def 3;
end;

theorem
  bool (A \ B) \/ bool (B \ A) c= bool (A \+\ B)
proof
  let x;
   reconsider xx=x as set by TARSKI:1;
  assume x in bool (A \ B) \/ bool (B \ A);
  then x in bool (A \ B) or x in bool (B \ A) by XBOOLE_0:def 3;
  then
A1: xx c= A \ B or xx c= B \ A by Def1;
  xx c= (A \ B) \/ (B \ A)
  proof
    let z;
    assume z in xx;
    then z in A \ B or z in B \ A by A1;
    hence thesis by XBOOLE_0:def 3;
  end;
  hence thesis by Def1;
end;

::
::  Union of a set.
::

theorem
  X in A implies X c= union A by Lm14;

theorem
  union { X,Y } = X \/ Y by Lm15;

theorem
  (for X st X in A holds X c= Z) implies union A c= Z
proof
  assume
A1: for X st X in A holds X c= Z;
  let y;
  assume y in union A;
  then consider Y such that
A2: y in Y and
A3: Y in A by TARSKI:def 4;
  Y c= Z by A1,A3;
  hence thesis by A2;
end;

theorem Th76:
  A c= B implies union A c= union B
proof
  assume
A1: A c= B;
  let x;
  assume x in union A;
  then consider Y such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
  Y in B by A1,A3;
  hence thesis by A2,TARSKI:def 4;
end;

theorem
  union (A \/ B) = union A \/ union B
proof
A1: union (A \/ B) c= union A \/ union B
  proof
    let x;
    assume x in union (A \/ B);
    then consider Y such that
A2: x in Y and
A3: Y in A \/ B by TARSKI:def 4;
    Y in A or Y in B by A3,XBOOLE_0:def 3;
    then x in union A or x in union B by A2,TARSKI:def 4;
    hence thesis by XBOOLE_0:def 3;
  end;
  union A c= union (A \/ B) & union B c= union (A \/ B) by Th76,XBOOLE_1:7;
  hence thesis by A1,XBOOLE_1:8;
end;

theorem Th78:
  union (A /\ B) c= union A /\ union B
proof
  let x;
  assume x in union (A /\ B);
  then consider Y such that
A1: x in Y and
A2: Y in A /\ B by TARSKI:def 4;
  Y in B by A2,XBOOLE_0:def 4;
  then
A3: x in union B by A1,TARSKI:def 4;
  Y in A by A2,XBOOLE_0:def 4;
  then x in union A by A1,TARSKI:def 4;
  hence thesis by A3,XBOOLE_0:def 4;
end;

theorem Th79:
  (for X st X in A holds X misses B) implies union A misses B
proof
  assume
A1: for X st X in A holds X misses B;
  assume union(A) meets B;
  then consider z such that
A2: z in union(A) /\ B by XBOOLE_0:4;
  z in union(A) by A2,XBOOLE_0:def 4;
  then consider X such that
A3: z in X and
A4: X in A by TARSKI:def 4;
  z in B by A2,XBOOLE_0:def 4;
  then z in X /\ B by A3,XBOOLE_0:def 4;
  hence contradiction by A1,A4,XBOOLE_0:4;
end;

theorem
  union bool A = A
proof
  now
    let x;
    thus x in union bool A implies x in A
    proof
      assume x in union bool A;
      then consider X such that
A1:   x in X and
A2:   X in bool A by TARSKI:def 4;
      X c= A by A2,Def1;
      hence thesis by A1;
    end;
    assume x in A;
    then { x } c= A by Lm1;
    then
A3: { x } in bool A by Def1;
    x in { x } by TARSKI:def 1;
    hence x in union bool A by A3,TARSKI:def 4;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  A c= bool union A
proof
  let x;
   reconsider xx=x as set by TARSKI:1;
  assume x in A;
  then xx c= union A by Lm14;
  hence thesis by Def1;
end;

theorem
  (for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y) implies
  union(A /\ B) = union A /\ union B
proof
  assume
A1: for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y;
 union A /\ union B c= union (A /\ B)
  proof
    let x;
    assume
A2: x in union A /\ union B;
    then x in union A by XBOOLE_0:def 4;
    then consider X such that
A3: x in X and
A4: X in A by TARSKI:def 4;
    x in union B by A2,XBOOLE_0:def 4;
    then consider Y such that
A5: x in Y and
A6: Y in B by TARSKI:def 4;
    now
A7:   x in X /\ Y by A3,A5,XBOOLE_0:def 4;
      assume
A8:   X<>Y;
      X in A \/ B & Y in A \/ B by A4,A6,XBOOLE_0:def 3;
      hence contradiction by A1,A8,A7,XBOOLE_0:4;
    end;
    then Y in A /\ B by A4,A6,XBOOLE_0:def 4;
    hence thesis by A5,TARSKI:def 4;
  end;
  hence thesis by Th78;
end;

::
::  Cartesian product.
::

theorem Th83:
  A c= [:X,Y:] & z in A implies
    ex x,y st x in X & y in Y & z = [ x,y]
proof
  assume A c= [:X,Y:] & z in A;
  then z in [:X,Y:];
  hence thesis by Def2;
end;

theorem Th84:
  z in [:X1, Y1:] /\ [:X2, Y2:] implies ex x,y st z = [x,y] & x
  in X1 /\ X2 & y in Y1 /\ Y2
proof
  assume
A1: z in [:X1, Y1:] /\ [:X2, Y2:];
  then z in [:X1, Y1:] by XBOOLE_0:def 4;
  then consider x1,y1 such that
A2: x1 in X1 and
A3: y1 in Y1 and
A4: z=[x1,y1] by Def2;
  z in [:X2, Y2:] by A1,XBOOLE_0:def 4;
  then consider x2,y2 such that
A5: x2 in X2 and
A6: y2 in Y2 and
A7: z=[x2,y2] by Def2;
  y1=y2 by A4,A7,XTUPLE_0:1;
  then
A8: y1 in Y1 /\ Y2 by A3,A6,XBOOLE_0:def 4;
  x1=x2 by A4,A7,XTUPLE_0:1;
  then x1 in X1 /\ X2 by A2,A5,XBOOLE_0:def 4;
  hence thesis by A4,A8;
end;

theorem
  [:X,Y:] c= bool bool (X \/ Y)
proof
  let z;
   reconsider zz=z as set by TARSKI:1;
  assume z in [:X,Y:];
  then consider x,y such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by Def2;
  zz c= bool (X \/ Y)
  proof
    let u;
    assume u in zz;
    then
A4: u = {x,y} or u = {x} by A3,TARSKI:def 2;
    X c= X \/ Y & {x} c= X by A1,Lm1,XBOOLE_1:7;
    then
A5: {x} c= X \/ Y;
    x in X \/ Y & y in X \/ Y by A1,A2,XBOOLE_0:def 3;
    then {x,y} c= X \/ Y by Th31;
    hence thesis by A5,A4,Def1;
  end;
  hence thesis by Def1;
end;

theorem
 for x,y being object holds [x,y] in [:X,Y:] iff x in X & y in Y by Lm16;

theorem Th87:
  [x,y] in [:X,Y:] implies [y,x] in [:Y,X:]
proof
  [x,y] in [:X,Y:] implies x in X & y in Y by Lm16;
  hence thesis by Lm16;
end;

theorem
  (for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:]) implies [:X1
  ,Y1:]=[:X2,Y2:]
proof
  assume
A1: for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:];
  now
    let z;
    thus z in [:X1,Y1:] implies z in [:X2,Y2:]
    proof
      assume
A2:   z in [:X1,Y1:];
      then ex x,y st x in X1 & y in Y1 & [x,y]=z by Def2;
      hence thesis by A1,A2;
    end;
    assume
A3: z in [:X2,Y2:];
    then ex x,y st x in X2 & y in Y2 & [x,y]=z by Def2;
    hence z in [:X1,Y1:] by A1,A3;
  end;
  hence thesis by TARSKI:2;
end;

Lm17: A c= [:X1,Y1:] & B c= [:X2,Y2:] & (for x,y holds [x,y] in A iff [x,y] in
B) implies A = B
proof
  assume that
A1: A c= [:X1,Y1:] and
A2: B c= [:X2,Y2:] and
A3: for x,y holds [x,y] in A iff [x,y] in B;
  now
    let z;
A4: z in B implies ex x,y st x in X2 & y in Y2 & z=[x,y] by A2,Th83;
    z in A implies ex x,y st x in X1 & y in Y1 & z=[x,y] by A1,Th83;
    hence z in A iff z in B by A3,A4;
  end;
  hence thesis by TARSKI:2;
end;

Lm18: ( for z st z in A ex x,y st z = [x,y]) & (for z st z in B ex x,y st z=[x
,y]) & (for x,y holds [x,y] in A iff [x,y] in B) implies A = B
proof
  assume that
A1: for z st z in A ex x,y st z=[x,y] and
A2: for z st z in B ex x,y st z=[x,y] and
A3: for x,y holds [x,y] in A iff [x,y] in B;
  now
    let z;
A4: z in B implies ex x,y st z=[x, y ] by A2;
    z in A implies ex x,y st z=[x,y] by A1;
    hence z in A iff z in B by A3,A4;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th89:
  [:X,Y:] = {} iff X = {} or Y = {}
proof
  thus [:X,Y:] = {} implies X={} or Y={}
  proof
    assume
A1: [:X,Y:] = {};
    assume X<>{};
    then consider x such that
A2: x in X by XBOOLE_0:7;
    assume Y<>{};
    then consider y such that
A3: y in Y by XBOOLE_0:7;
    [x,y] in [:X,Y:] by A2,A3,Def2;
    hence contradiction by A1;
  end;
  assume
A4: not thesis;
  then consider z such that
A5: z in [:X,Y:] by XBOOLE_0:7;
  ex x,y st x in X & y in Y & [x,y]=z by A5,Def2;
 hence contradiction by A4;
end;

theorem
  X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y
proof
  assume X<>{};
  then consider x such that
A1: x in X by XBOOLE_0:7;
  assume Y<>{};
  then consider y such that
A2: y in Y by XBOOLE_0:7;
  assume
A3: [:X,Y:]=[:Y,X:];
  for z holds z in X iff z in Y
  proof let z;
    thus z in X implies z in Y
    proof
      assume z in X;
      then [z,y] in [:Y,X:] by A2,A3,Lm16;
      hence thesis by Lm16;
    end;
    assume z in Y;
    then [z,x] in [:X,Y:] by A1,A3,Lm16;
    hence thesis by Lm16;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  [:X,X:] = [:Y,Y:] implies X = Y
proof
  assume
A1: [:X,X:] = [:Y,Y:];
  for x holds x in X iff x in Y
  proof let x;
    x in X iff [x,x] in [:X,X:] by Lm16;
    hence thesis by A1,Lm16;
  end;
  hence thesis by TARSKI:2;
end;

Lm19: z in [:X,Y:] implies ex x,y st [x,y] = z
proof
  assume z in [:X,Y:];
  then ex x,y st x in X & y in Y & [x,y]=z by Def2;
  hence thesis;
end;

theorem
  X c= [:X,Y:] implies X = {}
proof
  assume
A1: X c= [:X,Y:];
  assume X <> {};
  then consider z such that
A2: z in X by XBOOLE_0:7;
  consider M such that
A3: M in X \/ union X and
A4: X \/ union X misses M by A2,XREGULAR:1;
  now
    assume
A5: M in X;
    then consider x,y such that
A6: M = [x,y] by Lm19,A1;
A7: {x} in M by A6,TARSKI:def 2;
    M c= union X by A5,Lm14;
    then {x} in union X by A7;
    then {x} in X \/ union X by XBOOLE_0:def 3;
    hence contradiction by A4,A7,XBOOLE_0:3;
  end;
  then M in union X by A3,XBOOLE_0:def 3;
  then consider Z such that
A8: M in Z and
A9: Z in X by TARSKI:def 4;
  Z in [:X,Y:] by A1,A9;
  then consider x,y such that
A10: x in X and y in Y and
A11: Z = [x,y] by Def2;
  M={x} or M={x,y} by A8,A11,TARSKI:def 2;
  then
A12: x in M by TARSKI:def 1,def 2;
  x in X \/ union X by A10,XBOOLE_0:def 3;
  hence contradiction by A4,A12,XBOOLE_0:3;
end;

theorem
  Z <> {} & ([:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:]) implies X c= Y
proof
  assume Z<>{};
  then consider z such that
A1: z in Z by XBOOLE_0:7;
  assume
A2: [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:];
  let x;
  assume x in X;
  then [x,z] in [:X,Z:] & [z,x] in [:Z,X:] by A1,Def2;
  then [x,z] in [:Y,Z:] or [z,x] in [:Z,Y:] by A2;
  hence thesis by Lm16;
end;

theorem Th94:
  X c= Y implies [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:]
proof
  assume
A1: X c= Y;
  thus [:X,Z:] c= [:Y,Z:]
  proof
    let z;
    assume z in [:X,Z:];
    then consider x,y such that
A2: x in X and
A3: y in Z & z=[x,y] by Def2;
    x in Y by A1,A2;
    hence thesis by A3,Def2;
  end;
  let z;
  assume z in [:Z,X:];
  then consider y,x such that
A4: y in Z and
A5: x in X and
A6: z=[y,x] by Def2;
  x in Y by A1,A5;
  hence thesis by A4,A6,Def2;
end;

theorem Th95:
  X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:]
proof
  assume X1 c= Y1 & X2 c= Y2;
  then [:X1,X2:] c= [:Y1,X2:] & [:Y1,X2:] c= [:Y1,Y2:] by Th94;
  hence thesis;
end;

theorem Th96:
  [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] & [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:]
proof
A1: for z st z in [:X \/ Y, Z:] ex x,y st z=[x,y] by Lm19;
A2: for x,y holds [x,y] in [:X \/ Y, Z:] iff [x,y] in [:X, Z:] \/ [:Y, Z:]
  proof
    let x,y;
    thus [x,y] in [:X \/ Y, Z:] implies [x,y] in [:X, Z:] \/ [:Y, Z:]
    proof
      assume
A3:   [x,y] in [:X \/ Y, Z:];
      then x in X \/ Y by Lm16;
      then
A4:   x in X or x in Y by XBOOLE_0:def 3;
      y in Z by A3,Lm16;
      then [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] by A4,Lm16;
      hence thesis by XBOOLE_0:def 3;
    end;
    assume [x,y] in [:X, Z:] \/ [:Y, Z:];
    then [x,y] in [:X, Z:] or [x,y] in [:Y, Z:] by XBOOLE_0:def 3;
    then
A5: x in X & y in Z or x in Y & y in Z by Lm16;
    then x in X \/ Y by XBOOLE_0:def 3;
    hence thesis by A5,Lm16;
  end;
A6: z in [:X1,X2:] \/ [:Y1,Y2:] implies ex x,y st z=[x,y]
  proof
    assume z in [:X1,X2:] \/ [:Y1,Y2:];
    then z in [:X1,X2:] or z in [:Y1,Y2:] by XBOOLE_0:def 3;
    hence thesis by Lm19;
  end;
  then for z st z in [:X,Z:] \/ [:Y,Z:] ex x,y st z=[x,y];
  hence
A7: [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] by A1,A2,Lm18;
A8: for y,x holds [y,x] in [:Z, X \/ Y:] iff [y,x] in [:Z, X:] \/ [:Z, Y:]
  proof
    let y,x;
A9: [x,y]in[:X, Z:] or [x,y]in[:Y,Z:] iff [y,x]in[:Z,X:] or [y,x]in[:Z,Y
    :] by Th87;
    [y,x] in [:Z, X \/ Y:] iff [x,y] in [:X \/ Y, Z:] by Th87;
    hence thesis by A7,A9,XBOOLE_0:def 3;
  end;
A10: for z st z in [:Z,X \/ Y:] ex x,y st z=[x,y] by Lm19;
  for z st z in [:Z,X:] \/ [:Z,Y:] ex x,y st z=[x,y] by A6;
  hence thesis by A10,A8,Lm18;
end;

theorem
  [:X1 \/ X2, Y1 \/ Y2:] = [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2, Y2:]
proof
  thus [:X1 \/ X2, Y1 \/ Y2:] = [:X1, Y1 \/ Y2:] \/ [:X2, Y1 \/ Y2:] by Th96
    .= [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1 \/ Y2:] by Th96
    .= [:X1,Y1:] \/ [:X1,Y2:] \/ ([:X2,Y1:] \/ [:X2,Y2:]) by Th96
    .= [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2,Y2:] by XBOOLE_1:4;
end;

theorem
  [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] & [:Z, X /\ Y:] = [:Z, X:] /\ [:Z , Y :]
proof
A1: for x,y holds [x,y] in [:X /\ Y, Z:] iff [x,y] in [:X, Z:] /\ [:Y, Z :]
  proof
    let x,y;
    thus [x,y] in [:X /\ Y, Z:] implies [x,y] in [:X, Z:] /\ [:Y, Z:]
    proof
      assume
A2:   [x,y] in [:X /\ Y, Z:];
      then
A3:   x in X /\ Y by Lm16;
A4:   y in Z by A2,Lm16;
      x in Y by A3,XBOOLE_0:def 4;
      then
A5:   [x,y] in [:Y,Z:] by A4,Lm16;
      x in X by A3,XBOOLE_0:def 4;
      then [x,y] in [:X,Z:] by A4,Lm16;
      hence thesis by A5,XBOOLE_0:def 4;
    end;
    assume
A6: [x,y] in [:X, Z:] /\ [:Y, Z:];
    then [x,y] in [:Y, Z:] by XBOOLE_0:def 4;
    then
A7: x in Y by Lm16;
A8: [x,y] in [:X, Z:] by A6,XBOOLE_0:def 4;
    then x in X by Lm16;
    then
A9: x in X /\ Y by A7,XBOOLE_0:def 4;
    y in Z by A8,Lm16;
    hence thesis by A9,Lm16;
  end;
  [:X, Z:] /\ [:Y, Z:] c= [:X, Z:] by XBOOLE_1:17;
  hence
A10: [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] by A1,Lm17;
A11: for y,x holds [y,x] in [:Z, X /\ Y:] iff [y,x] in [:Z, X:] /\ [:Z, Y:]
  proof
    let y,x;
A12: [x,y]in[:X, Z:] & [x,y]in[:Y,Z:] iff [y,x]in[:Z,X:] & [y,x]in[:Z,Y:]
    by Th87;
    [y,x] in [:Z, X /\ Y:] iff [x,y] in [:X /\ Y, Z:] by Th87;
    hence thesis by A10,A12,XBOOLE_0:def 4;
  end;
  [:Z, X:] /\ [:Z, Y:] c= [:Z, X:] by XBOOLE_1:17;
  hence thesis by A11,Lm17;
end;

theorem Th99:
  [:X1 /\ X2, Y1 /\ Y2:] = [:X1,Y1:] /\ [:X2, Y2:]
proof
  Y1 /\ Y2 c= Y2 & X1 /\ X2 c= X2 by XBOOLE_1:17;
  then
A1: [:X1 /\ X2, Y1 /\ Y2:] c= [:X2, Y2:] by Th95;
A2: [:X1, Y1:] /\ [:X2, Y2:] c= [:X1 /\ X2, Y1 /\ Y2:]
  proof
    let z;
    assume z in [:X1, Y1:] /\ [:X2, Y2:];
    then ex x,y st z=[x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 by Th84;
    hence thesis by Def2;
  end;
  Y1 /\ Y2 c= Y1 & X1 /\ X2 c= X1 by XBOOLE_1:17;
  then [:X1 /\ X2, Y1 /\ Y2:] c= [:X1, Y1:] by Th95;
  hence thesis by A2,A1,XBOOLE_1:19;
end;

theorem
  A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:]
proof
  assume that
A1: A c= X and
A2: B c= Y;
A3: [:A,Y:] /\ [:X,B:] = [:A /\ X, Y /\ B:] by Th99;
  A /\ X = A by A1,XBOOLE_1:28;
  hence thesis by A2,A3,XBOOLE_1:28;
end;

theorem Th101:
  [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] & [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:]
proof
A1: for x,y holds [x,y] in [:X \ Y, Z:] iff [x,y] in [:X, Z:] \ [:Y, Z:]
  proof
    let x,y;
    thus [x,y] in [:X \ Y, Z:] implies [x,y] in [:X, Z:] \ [:Y, Z:]
    proof
      assume
A2:   [x,y] in [:X \ Y, Z:];
      then
A3:   x in X \ Y by Lm16;
      then
A4:   x in X by XBOOLE_0:def 5;
      not x in Y by A3,XBOOLE_0:def 5;
      then
A5:   not [x,y] in [:Y,Z:] by Lm16;
      y in Z by A2,Lm16;
      then [x,y] in [:X,Z:] by A4,Lm16;
      hence thesis by A5,XBOOLE_0:def 5;
    end;
    assume
A6: [x,y] in [:X, Z:] \ [:Y, Z:];
    then
A7: [x,y] in [:X, Z:] by XBOOLE_0:def 5;
    then
A8: y in Z by Lm16;
    not [x,y] in [:Y, Z:] by A6,XBOOLE_0:def 5;
    then
A9: not (x in Y & y in Z) by Lm16;
    x in X by A7,Lm16;
    then x in X \ Y by A7,A9,Lm16,XBOOLE_0:def 5;
    hence thesis by A8,Lm16;
  end;
  [:X, Z:] \ [:Y, Z:] c= [:X, Z:] by XBOOLE_1:36;
  hence
A10: [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] by A1,Lm17;
A11: for y,x holds [y,x] in [:Z, X \ Y:] iff [y,x] in [:Z, X:] \ [:Z, Y:]
  proof
    let y,x;
A12: [x,y]in[:X, Z:]& not[x,y]in[:Y,Z:] iff [y,x]in[:Z,X:]& not[y,x]in[:Z,
    Y :] by Th87;
    [y,x] in [:Z, X \ Y:] iff [x,y] in [:X \ Y, Z:] by Th87;
    hence thesis by A10,A12,XBOOLE_0:def 5;
  end;
  [:Z, X:] \ [:Z, Y:] c= [:Z, X:] by XBOOLE_1:36;
  hence thesis by A11,Lm17;
end;

theorem
  [:X1,X2:] \ [:Y1,Y2:] = [:X1\Y1,X2:] \/ [:X1,X2\Y2:]
proof
A1: [:Y1,X2:] /\ [:X1,Y2:] = [:Y1 /\ X1, X2 /\ Y2:] by Th99;
  Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 by XBOOLE_1:17;
  then
A2: [:Y1 /\ X1, X2 /\ Y2:] c= [:Y1,Y2:] by Th95;
A3: [:X1\Y1,X2:] \/ [:X1,X2\Y2:] c= [:X1,X2:] \ [:Y1, Y2:]
  proof
    let z;
A4: now
      assume z in [:X1\Y1,X2:];
      then consider x,y such that
A5:   x in X1\Y1 and
A6:   y in X2 and
A7:   z=[x,y] by Def2;
      not x in Y1 by A5,XBOOLE_0:def 5;
      then
A8:   not z in [:Y1,Y2:] by A7,Lm16;
      x in X1 by A5,XBOOLE_0:def 5;
      then z in [:X1,X2:] by A6,A7,Lm16;
      hence thesis by A8,XBOOLE_0:def 5;
    end;
A9: now
      assume z in [:X1,X2\Y2:];
      then consider x,y such that
A10:  x in X1 and
A11:  y in X2\Y2 and
A12:  z=[x,y] by Def2;
      not y in Y2 by A11,XBOOLE_0:def 5;
      then
A13:  not z in [:Y1,Y2:] by A12,Lm16;
      y in X2 by A11,XBOOLE_0:def 5;
      then z in [:X1,X2:] by A10,A12,Lm16;
      hence thesis by A13,XBOOLE_0:def 5;
    end;
    assume z in [:X1\Y1,X2:] \/ [:X1,X2\Y2:];
    hence thesis by A4,A9,XBOOLE_0:def 3;
  end;
  [:X1\Y1,X2:] = [:X1,X2:] \ [:Y1,X2:] & [:X1,X2\Y2:] = [:X1,X2:] \ [:X1,
  Y2 :] by Th101;
  then [:X1\Y1,X2:] \/ [:X1,X2\Y2:] = [:X1,X2:] \ [:Y1 /\ X1, X2 /\ Y2:] by A1,
XBOOLE_1:54;
  hence thesis by A3,A2,XBOOLE_1:34;
end;

theorem Th103:
  X1 misses X2 or Y1 misses Y2 implies [:X1,Y1:] misses [:X2,Y2:]
proof
  assume
A1: X1 misses X2 or Y1 misses Y2;
  assume not thesis;
  then consider z such that
A2: z in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:4;
  ex x,y st z=[x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 by A2,Th84;
  hence contradiction by A1;
end;

theorem
  [x,y] in [:{z},Y:] iff x = z & y in Y
proof
A1: x in {z} iff x=z by TARSKI:def 1;
  hence [x,y] in [:{z},Y:] implies x=z & y in Y by Lm16;
  thus thesis by A1,Lm16;
end;

theorem
  [x,y] in [:X,{z}:] iff x in X & y = z
proof
A1: y in {z} iff y=z by TARSKI:def 1;
  hence [x,y] in [:X,{z}:] implies x in X & y=z by Lm16;
  thus thesis by A1,Lm16;
end;

theorem
  X <> {} implies [:{x},X:] <> {} & [:X,{x}:] <> {} by Th89;

theorem
  x <> y implies [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:]
proof
  assume x<>y;
  then {x} misses {y} by Th11;
  hence thesis by Th103;
end;

theorem
  [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X, {y} :]
proof
  {x,y}={x} \/ {y} by ENUMSET1:1;
  hence thesis by Th96;
end;

theorem Th109:
  X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies X1 = X2 & Y1 = Y2
proof
  assume
A1: X1<>{};
  then consider x such that
A2: x in X1 by XBOOLE_0:7;
  assume
A3: Y1<>{};
  then consider y such that
A4: y in Y1 by XBOOLE_0:7;
  assume
A5: [:X1,Y1:] = [:X2,Y2:];
  then
A6: [:X2,Y2:] <> {} by A1,A3,Th89;
  then
A7: Y2 <> {} by Th89;
  for z holds z in X1 iff z in X2
  proof let z;
    consider y2 such that
A8: y2 in Y2 by A7,XBOOLE_0:7;
    thus z in X1 implies z in X2
    proof
      assume z in X1;
      then [z,y] in [:X2,Y2:] by A4,A5,Lm16;
      hence thesis by Lm16;
    end;
    assume z in X2;
    then [z,y2] in [:X2,Y2:] by A8,Lm16;
    hence thesis by A5,Lm16;
  end;
  hence X1 = X2 by TARSKI:2;
A9: X2 <> {} by A6,Th89;
  for z holds z in Y1 iff z in Y2
  proof let z;
    consider x2 such that
A10: x2 in X2 by A9,XBOOLE_0:7;
    thus z in Y1 implies z in Y2
    proof
      assume z in Y1;
      then [x,z] in [:X2,Y2:] by A2,A5,Lm16;
      hence thesis by Lm16;
    end;
    assume z in Y2;
    then [x2,z] in [:X2,Y2:] by A10,Lm16;
    hence thesis by A5,Lm16;
  end;
  hence thesis by TARSKI:2;
end;

theorem
  X c= [:X,Y:] or X c= [:Y,X:] implies X = {}
proof
  assume
A1: X c= [:X,Y:] or X c= [:Y,X:];
  assume
A2: X <> {};
A3: now
    defpred P[object] means ex Y st $1=Y & ex z st z in Y & z in X;
    consider Z such that
A4: for y holds y in Z iff y in union X & P[y] from XBOOLE_0:sch 1;
    consider Y2 such that
A5: Y2 in X \/ Z and
A6: X \/ Z misses Y2 by A2,XREGULAR:1;
    now
      assume
A7:   not ex Y2 st Y2 in X & for Y1 st Y1 in Y2 holds for z holds not
      z in Y1 or not z in X;
      now
        assume
A8:     Y2 in X;
        then consider Y1 such that
A9:     Y1 in Y2 and
A10:    ex z st z in Y1 & z in X by A7;
        Y1 in union X by A8,A9,TARSKI:def 4;
        then Y1 in Z by A4,A10;
        then Y1 in X \/ Z by XBOOLE_0:def 3;
        hence contradiction by A6,A9,XBOOLE_0:3;
      end;
      then Y2 in Z by A5,XBOOLE_0:def 3;
      then ex X2 st Y2=X2 & ex z st z in X2 & z in X by A4;
      then consider z such that
A11:  z in Y2 and
A12:  z in X;
      z in X \/ Z by A12,XBOOLE_0:def 3;
      hence contradiction by A6,A11,XBOOLE_0:3;
    end;
    then consider Y1 such that
A13: Y1 in X and
A14: not ex Y2 st Y2 in Y1 & ex z st z in Y2 & z in X;
A15: now
      given y,x such that
A16:  x in X and
A17:  Y1 = [y,x];
A18:  x in {y,x} by TARSKI:def 2;
      {y,x} in Y1 by A17,TARSKI:def 2;
      hence contradiction by A14,A16,A18;
    end;
    assume X c= [:Y,X:];
    then Y1 in [:Y,X:] by A13;
    then ex y,x being object st y in Y & x in X & Y1 = [y,x] by Def2;
    hence contradiction by A15;
  end;
  now
    consider z being object such that
A19: z in X by A2,XBOOLE_0:7;
    consider Y1 such that
A20: Y1 in X \/ union X and
A21: X \/ union X misses Y1 by A19,XREGULAR:1;
    assume
A22: X c= [:X,Y:];
    now
      assume
A23:  Y1 in X;
      then consider x,y such that
A24:  Y1 = [x,y] by Lm19,A22;
A25:  {x} in Y1 by A24,TARSKI:def 2;
      Y1 c= union X by A23,Lm14;
      then {x} in union X by A25;
      then {x} in X \/ union X by XBOOLE_0:def 3;
      hence contradiction by A21,A25,XBOOLE_0:3;
    end;
    then Y1 in union X by A20,XBOOLE_0:def 3;
    then consider Y2 such that
A26: Y1 in Y2 and
A27: Y2 in X by TARSKI:def 4;
    Y2 in [:X,Y:] by A22,A27;
    then consider x,y being object such that
A28: x in X and
    y in Y and
A29: Y2=[x,y] by Def2;
    Y1={x} or Y1={x,y} by A26,A29,TARSKI:def 2;
    then
A30: x in Y1 by TARSKI:def 1,def 2;
    x in X \/ union X by A28,XBOOLE_0:def 3;
    hence contradiction by A21,A30,XBOOLE_0:3;
  end;
  hence thesis by A1,A3;
end;

theorem
  ex M st N in M & (for X,Y holds X in M & Y c= X implies Y in M) & (for
  X holds X in M implies bool X in M) & for X holds X c= M implies X,M
  are_equipotent or X in M
proof
  consider M such that
A1: N in M and
A2: for X,Y holds X in M & Y c= X implies Y in M and
A3: for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z and
A4: for X holds X c= M implies X,M are_equipotent or X in M by TARSKI_A:1;
  take M;
  thus N in M by A1;
  thus for X,Y holds X in M & Y c= X implies Y in M by A2;
  thus for X holds X in M implies bool X in M
  proof
    let X;
    assume X in M;
    then consider Z such that
A5: Z in M and
A6: for Y st Y c= X holds Y in Z by A3;
    now
      let Y be object;
   reconsider YY=Y as set by TARSKI:1;
      assume Y in bool X;
      then YY c= X by Def1;
      hence Y in Z by A6;
    end;
    hence thesis by A2,A5,TARSKI:def 3;
  end;
  thus thesis by A4;
end;

reserve e for object, X,X1,X2,Y1,Y2 for set;

theorem
  e in [:X1,Y1:] & e in [:X2,Y2:] implies e in [:X1 /\ X2, Y1 /\ Y2:]
proof
  assume e in [:X1,Y1:] & e in [:X2,Y2:];
  then e in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:def 4;
  hence thesis by Th99;
end;

begin :: Addenda
:: from BORSUK_1

theorem Th113:
  [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} implies X1 c= Y1 & X2 c= Y2
proof
  assume that
A1: [:X1,X2:] c= [:Y1,Y2:] and
A2: [:X1,X2:] <> {};
A3: [:X1,X2:] = [:X1,X2:] /\ [:Y1,Y2:] by A1,XBOOLE_1:28
    .= [:X1/\Y1,X2/\Y2:] by Th99;
  X1 <> {} & X2 <> {} by A2,Th89;
  then X1 = X1/\Y1 & X2 = X2/\Y2 by A3,Th109;
  hence thesis by XBOOLE_1:17;
end;

:: from ALTCAT_1

theorem
  for A being non empty set, B,C,D being set st [:A,B:] c= [:C,D:] or [:
  B,A:] c= [:D,C:] holds B c= D
proof
  let A be non empty set, B,C,D be set such that
A1: [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:];
  per cases;
  suppose
    B = {};
    hence thesis;
  end;
  suppose
    B <> {};
    then [:A,B:] <> {} & [:B,A:] <> {} by Th89;
    hence thesis by A1,Th113;
  end;
end;

theorem
  x in X implies (X\{x})\/{x}=X
proof
  assume
A1: x in X;
  thus (X\{x})\/{x}c=X
  proof
    let y be object;
    assume y in (X\{x})\/{x};
    then y in X\{x} or y in {x} by XBOOLE_0:def 3;
    hence thesis by A1,Th55,TARSKI:def 1;
  end;
  thus X c= (X\{x})\/{x}
  proof
    let y be object;
    assume y in X;
    then y in {x} or y in X\{x} by XBOOLE_0:def 5;
    hence thesis by XBOOLE_0:def 3;
  end;
end;

theorem
  not x in X implies (X\/{x})\{x}=X
proof
A1: (X \/ {x}) \ {x} = X \ {x} by XBOOLE_1:40;
  assume not x in X;
  hence thesis by A1,Th56;
end;

:: from WAYBEL18, 2006.01.06, A.T.

theorem
  for x,y,z,Z being set holds Z c= {x,y,z} iff Z = {} or Z = {x} or Z =
  {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z}
proof
  let x,y,z,Z be set;
  hereby
    assume that
A1: Z c= {x,y,z} and
A2: Z <> {} and
A3: Z <> {x} and
A4: Z <> {y} and
A5: Z <> {z} and
A6: Z <> {x,y} and
A7: Z <> {y,z} and
A8: Z <> {x,z};
    {x,y,z} c= Z
    proof
      let a be object;
A9:   now
        {x,y,z} \ {x} = ({x} \/ {y,z}) \ {x} by ENUMSET1:2
          .= {y,z} \ {x} by XBOOLE_1:40;
        then
A10:    {x,y,z} \ {x} c= {y,z} by XBOOLE_1:36;
        assume not x in Z;
        then Z c= {x,y,z} \ {x} by A1,Lm2;
        hence contradiction by A2,A4,A5,A7,Lm13,A10,XBOOLE_1:1;
      end;
A11:  now
        {x,y,z} \ {y} = ({x,y} \/ {z}) \ {y} by ENUMSET1:3
          .= ({x} \/ {y} \/ {z}) \ {y} by ENUMSET1:1
          .= ({x} \/ {z} \/ {y}) \ {y} by XBOOLE_1:4
          .= ({x,z} \/ {y}) \ {y} by ENUMSET1:1
          .= {x,z} \ {y} by XBOOLE_1:40;
        then
A12:    {x,y,z} \ {y} c= {x,z} by XBOOLE_1:36;
        assume not y in Z;
        then Z c= {x,y,z} \ {y} by A1,Lm2;
        hence contradiction by A2,A3,A5,A8,Lm13,A12,XBOOLE_1:1;
      end;
A13:  now
        {x,y,z} \ {z} = ({x,y} \/ {z}) \ {z} by ENUMSET1:3
          .= {x,y} \ {z} by XBOOLE_1:40;
        then
A14:    {x,y,z} \ {z} c= {x,y} by XBOOLE_1:36;
        assume not z in Z;
        then Z c= {x,y,z} \ {z} by A1,Lm2;
        hence contradiction by A2,A3,A4,A6,Lm13,A14,XBOOLE_1:1;
      end;
      assume a in {x,y,z};
      hence thesis by A9,A11,A13,ENUMSET1:def 1;
    end;
    hence Z = {x,y,z} by A1;
  end;
  assume
A15: Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z}
  or Z = {x,z} or Z = {x,y,z};
  per cases by A15;
  suppose
    Z = {};
    hence thesis;
  end;
  suppose
    Z = {x};
    then Z c= {x} \/ {y,z} by XBOOLE_1:7;
    hence thesis by ENUMSET1:2;
  end;
  suppose
A16: Z = {y};
    {x,y} c= {x,y} \/ {z} by XBOOLE_1:7;
    then
A17: {x,y} c= {x,y,z} by ENUMSET1:3;
    Z c= {x,y} by A16,Th7;
    hence thesis by A17;
  end;
  suppose
    Z = {z};
    then Z c= {x,y} \/ {z} by XBOOLE_1:7;
    hence thesis by ENUMSET1:3;
  end;
  suppose
    Z = {x,y};
    then Z c= {x,y} \/ {z} by XBOOLE_1:7;
    hence thesis by ENUMSET1:3;
  end;
  suppose
    Z = {y,z};
    then Z c= {x} \/ {y,z} by XBOOLE_1:7;
    hence thesis by ENUMSET1:2;
  end;
  suppose
A18: Z = {x,z};
A19: {x,z} \/ {y} = {x} \/ {z} \/ {y} by ENUMSET1:1
      .= {x} \/ ({y} \/ {z}) by XBOOLE_1:4
      .= {x} \/ {y,z} by ENUMSET1:1;
    Z c= {x,z} \/ {y} by A18,XBOOLE_1:7;
    hence thesis by A19,ENUMSET1:2;
  end;
  suppose
    Z = {x,y,z};
    hence thesis;
  end;
end;

:: from PARTFUN1, 2006.12.05, A.T.

theorem
  N c= [:X1,Y1:] & M c= [:X2,Y2:] implies N \/ M c= [:X1 \/ X2,Y1 \/ Y2 :]
proof
  assume N c= [:X1,Y1:] & M c= [:X2,Y2:];
  then
A1: N \/ M c= [:X1,Y1:] \/ [:X2,Y2:] by XBOOLE_1:13;
  X1 c= X1 \/ X2 & Y1 c= Y1 \/ Y2 by XBOOLE_1:7;
  then
A2: [:X1,Y1:] c= [:X1 \/ X2,Y1 \/ Y2:] by Th95;
  Y2 c= Y1 \/ Y2 & X2 c= X1 \/ X2 by XBOOLE_1:7;
  then [:X2,Y2:] c= [:X1 \/ X2,Y1 \/ Y2:] by Th95;
  then [:X1,Y1:] \/ [:X2,Y2:] c= [:X1 \/ X2,Y1 \/ Y2:] by A2,XBOOLE_1:8;
  hence thesis by A1;
end;

Lm20: not x in X & not y in X implies {x,y} misses X
proof
  assume
A1: ( not x in X)& not y in X;
  thus {x,y} /\ X c= {}
  proof
    let z be object;
    assume z in {x,y} /\ X;
    then z in {x,y} & z in X by XBOOLE_0:def 4;
    hence thesis by A1,TARSKI:def 2;
  end;
  thus thesis;
end;

theorem Th119:
  not x in X & not y in X implies X = X \ {x,y}
proof
  X \ {x,y} = X iff X misses {x,y} by XBOOLE_1:83;
  hence thesis by Lm20;
end;

theorem
  not x in X & not y in X implies X = X \/ {x,y} \ {x,y}
proof
A1: (X \/ {x,y}) \ {x,y} = X \ {x,y} by XBOOLE_1:40;
  assume ( not x in X)& not y in X;
  hence thesis by A1,Th119;
end;

:: from INCPROJ, 2007.01.18. AK

definition
  let x1, x2, x3 be object;
  pred x1, x2, x3 are_mutually_distinct means
  x1 <> x2 & x1 <> x3 & x2 <> x3;
end;

definition
  let x1, x2, x3, x4 be object;
  pred x1, x2, x3, x4 are_mutually_distinct means
  x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;
end;

:: from CARD_2, 2007.01.18. AK

definition
  let x1, x2, x3, x4, x5 be object;
  pred x1, x2, x3, x4, x5 are_mutually_distinct means
  x1 <> x2 & x1 <> x3 &
x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4
  <> x5;
end;

:: from BORSUK_5, 2007.01.18. AK

definition
  let x1, x2, x3, x4, x5, x6 be object;
  pred x1, x2, x3, x4, x5, x6 are_mutually_distinct means
  x1 <> x2 & x1 <> x3
& x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 &
  x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6;
end;

definition
  let x1, x2, x3, x4, x5, x6, x7 be object;
  pred x1, x2, x3, x4, x5, x6, x7 are_mutually_distinct means
  x1 <> x2 & x1
<> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <>
x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5
  & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7;
end;

:: missing, 2007.02.11, A.T.

theorem
  [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof
  thus [:{x1,x2},{y1,y2}:] = [:{x1}\/{x2},{y1,y2}:] by ENUMSET1:1
    .= [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by Th96
    .= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by Th29
    .= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by Th29
    .= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5;
end;

:: missing, 2008.03.22, A.T.

theorem
  x <> y implies A \/ {x} \ {y} = A \ {y} \/ {x} by Th11,XBOOLE_1:87;

:: comp. REALSET1, 2008.07.05, A.T.

definition
  let X;
  attr X is trivial means
 x in X & y in X implies x = y;
end;

registration
  cluster empty -> trivial for set;
  coherence;
end;

registration
  cluster non trivial -> non empty for set;
  coherence;
end;

registration
  let x;
  cluster {x} -> trivial;
  coherence
  proof
    let y,z;
    assume that
A1: y in {x} and
A2: z in {x};
    y =x by A1,TARSKI:def 1;
    hence thesis by A2,TARSKI:def 1;
  end;
end;

registration
 cluster trivial non empty for set;
 existence
  proof
   take {{}};
   thus thesis;
  end;
end;

:: from SPRECT_3, 2008.09.30, A.T.

theorem
  for A,B,C being set, p be object
   st A c= B & B /\ C = {p} & p in A holds A /\ C = {p}
proof
  let A,B,C be set, p be object such that
A1: A c= B;
  assume
A2: B /\ C = {p};
  p in B /\ C by A2,TARSKI:def 1;
  then
A3: p in C by XBOOLE_0:def 4;
  assume p in A;
  then p in A /\ C by A3,XBOOLE_0:def 4;
  hence thesis by A2,Lm3,A1,XBOOLE_1:26;
end;

:: from SPRECT_2, 2008.09.30, A.T.

theorem
  for A,B,C being set st A /\ B c= {p} & p in C & C misses B holds A
  \/ C misses B
proof
  let A,B,C be set such that
A1: A /\ B c= {p} and
A2: p in C and
A3: C misses B;
  {p} c= C by A2,Lm1;
  then A /\ B c= C by A1;
  then A /\ B /\ B c= C /\ B by XBOOLE_1:27;
  then
A4: A /\ (B /\ B) c= C /\ B by XBOOLE_1:16;
  (A \/ C) /\ B = A /\ B \/ C /\ B by XBOOLE_1:23
    .= {} by A3,A4,XBOOLE_1:12;
  hence thesis;
end;

theorem
  for A,B being set st for x,y being set st x in A & y in B holds x
  misses y holds union A misses union B
proof
  let A,B be set such that
A1: for x,y being set st x in A & y in B holds x misses y;
  for y being set st y in B holds union A misses y
  proof
    let y be set;
    assume y in B;
    then for x being set st x in A holds x misses y by A1;
    hence thesis by Th79;
  end;
  hence thesis by Th79;
end;

:: from BORSUK_3, 2009.01.24, A.T.

registration
  let X be set, Y be empty set;
  cluster [:X, Y:] -> empty;
  coherence by Th89;
end;

registration
  let X be empty set, Y be set;
  cluster [:X, Y:] -> empty;
  coherence by Th89;
end;

:: new, 2009.08.26, A.T

theorem
 not A in [:A,B:]
  proof
   assume A in [:A,B:];
    then consider x,y being object such that
A1:   x in A & y in B & A = [x,y] by Th83;
    reconsider x as set by TARSKI:1;
    x = {x} or x = {x,y} by A1,TARSKI:def 2;
    then x in x by TARSKI:def 1,def 2;
   hence contradiction;
  end;

theorem
 B = [x,{x}] implies B in [:{x},B:]
  proof assume
A1:  B = [x,{x}];
    then [:{x},B:] = { [x,{x}], [x,{x,{x}}] } by Th29;
   hence thesis by TARSKI:def 2,A1;
  end;

theorem
 B in [:A,B:] implies ex x being object st x in A & B = [x,{x}]
  proof
   assume B in [:A,B:];
    then consider x,y being object such that
A1:   x in A & y in B & B = [x,y] by Th83;
   take x;
   thus x in A by A1;
   per cases by A1,TARSKI:def 2;
   suppose y = {x};
    hence thesis by A1;
   end;
   suppose
A2:   y = {x,y};
     reconsider y as set by TARSKI:1;
     y in y by TARSKI:def 2,A2;
    hence thesis;
   end;
  end;

theorem
 B c= A & A is trivial implies B is trivial
proof assume that
A1: B c= A and
A2: A is trivial;
  let x,y;
 assume x in B & y in B;
  then x in A & y in A by A1;
 hence thesis by A2;
end;

registration
  cluster non trivial for set;
  existence
  proof
   take {{},{{}}}, {},{{}};
   thus {} in {{},{{}}} & {{}} in  {{},{{}}} by TARSKI:def 2;
   thus {} <> {{}};
  end;
end;

theorem Th130:
 X is non empty trivial implies ex x st X = {x}
 proof
  assume X is non empty;
   then consider x being object such that
A1:  x in X;
  assume
A2:  X is trivial;
  take x;
  for y being object holds y in X iff x = y by A2,A1;
  hence thesis by TARSKI:def 1;
 end;

theorem
  for x being set, X being trivial set st x in X holds X = {x}
proof
  let x be set, X be trivial set;
  assume
A1: x in X;
  then ex x being object st X = {x} by Th130;
  hence thesis by A1,TARSKI:def 1;
end;

:: from JORDAN16, 2011.04.27, A.T.

theorem
  for a,b,c,X being set st a in X & b in X & c in X holds {a,b,c} c= X
proof
  let a,b,c,X be set;
  assume a in X & b in X & c in X;
  then {a,b} c= X & {c} c= X by Lm1,Th31;
  then {a,b} \/ {c} c= X by XBOOLE_1:8;
  hence thesis by ENUMSET1:3;
end;

:: Lemma from RELAT_1, FUNCT_4

theorem
 [x,y] in X implies x in union union X & y in union union X
proof
  assume
A1: [x,y] in X;
  { x } in {{x},{x,y}} by TARSKI:def 2;
  then
A2: {x} in union X by A1,TARSKI:def 4;
  {x,y} in {{x},{x,y}} by TARSKI:def 2;
  then
A3: {x,y} in union X by A1,TARSKI:def 4;
  y in {x,y} & x in {x} by TARSKI:def 1,def 2;
  hence thesis by A3,A2,TARSKI:def 4;
end;

theorem Th134:
  X c= Y \/ {x} implies x in X or X c= Y
proof
  assume that
A1: X c= Y \/ {x} and
A2: not x in X;
  X = X /\ (Y \/ {x}) by A1,XBOOLE_1:28
    .= X /\ Y \/ X /\ {x} by XBOOLE_1:23
    .= X /\ Y \/ {} by A2,Lm6,XBOOLE_0:def 7
    .= X /\ Y;
  hence thesis by XBOOLE_1:17;
end;

theorem
  x in X \/ {y} iff x in X or x = y
proof
  x in X \/ {y} iff x in X or x in {y} by XBOOLE_0:def 3;
  hence thesis by TARSKI:def 1;
end;

theorem
  X \/ {x} c= Y iff x in Y & X c= Y
proof
 X c= Y & {x} c= Y implies X \/ {x} c= Y by XBOOLE_1:8;
  hence thesis by Lm1,XBOOLE_1:11;
end;

theorem
  for A, B being set st A c= B & B c= A \/ {a} holds A \/ {a} = B or A = B
proof
  let A, B be set;
  assume that
A1: A c= B and
A2: B c= A \/ {a};
  assume that
A3: A \/ {a} <> B and
A4: A <> B;
 not a in B
  proof
    assume a in B;
    then {a} c= B by Lm1;
    hence thesis by A1,A2,A3,XBOOLE_1:8;
  end;
  hence thesis by A2,Th134,A1,A4;
end;

registration let A,B be trivial set;
 cluster [:A,B:] -> trivial;
 coherence
  proof
   per cases;
   suppose A is empty or B is empty;
    hence thesis;
   end;
   suppose that
A1: A is not empty and
A2: B is not empty;
   consider a being object such that
A3: A = {a} by A1,Th130;
   consider b being object such that
A4: B = {b} by A2,Th130;
     [:A,B:] = {[a,b]} by A3,A4,Th28;
    hence thesis;
   end;
  end;
end;

:: from REALSET1, 2012.08.12, A.T.

theorem
  for X being set holds X is non trivial iff
   for x holds X\{x} is non empty
proof
  let X be set;
  hereby
    assume
A1: X is non trivial;
    let x be object;
    X <> {x} by A1;
    then consider y being object such that
A2: y in X and
A3: x <> y by A1,Lm12;
    not y in {x} by A3,TARSKI:def 1;
    hence X\{x} is non empty by A2,XBOOLE_0:def 5;
  end;
  assume
A4: for x holds X\{x} is non empty;
   X\{{}} c= X by XBOOLE_1:36;
   then X is non empty by A4;
   then consider x being object such that
A5:  x in X;
   X\{x} is non empty by A4;
   then consider y being object such that
A6:  y in X\{x};
   reconsider x,y as set by TARSKI:1;
  take x,y;
  thus x in X by A5;
   X\{x} c= X by XBOOLE_1:36;
  hence y in X by A6;
   x in {x} by TARSKI:def 1;
  hence x <> y by A6,XBOOLE_0:def 5;
end;

theorem
  {X} <> X
  proof
    X in {X} by TARSKI:def 1;
    hence thesis;
  end;

theorem
  bool X <> X
  proof
    X in bool X by Def1;
    hence thesis;
  end;