:: Enumerated Sets
::  by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990-2012 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 TARSKI, XBOOLE_0;
 notations TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 definitions TARSKI, XBOOLE_0;
 theorems TARSKI, XBOOLE_0, XBOOLE_1;
 schemes XBOOLE_0;

begin

reserve x,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,y,X,Z for set;

Lm1: x in union({X,{y}}) iff x in X or x=y
proof
A1: 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;
A2: x in {y} iff x=y by TARSKI:def 1;
  X in {X,{y}} & {y} in {X,{y}} by TARSKI:def 2;
  hence thesis by A1,A2,TARSKI:def 4;
end;

definition
  let x1,x2,x3;
  func { x1,x2,x3 } -> set means
  :Def1:
  x in it iff x=x1 or x=x2 or x=x3;
  existence
  proof
    take union({{x1,x2},{x3}});
    let x;
    x in { x1,x2 } iff x = x1 or x = x2 by TARSKI:def 2;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

definition
  let x1,x2,x3,x4;
  func { x1,x2,x3,x4 } -> set means
  :Def2:
  x in it iff x=x1 or x=x2 or x=x3 or x=x4;
  existence
  proof
    take union({{x1,x2,x3},{x4}});
    let x;
    x in { x1,x2,x3 } iff x = x1 or x = x2 or x = x3 by Def1;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

definition
  let x1,x2,x3,x4,x5;
  func { x1,x2,x3,x4,x5 } -> set means
  :Def3:
  x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5;
  existence
  proof
    take union({{x1,x2,x3,x4},{x5}});
    let x;
    x in { x1,x2,x3,x4 } iff x = x1 or x = x2 or x = x3 or x = x4 by Def2;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

definition
  let x1,x2,x3,x4,x5,x6;
  func { x1,x2,x3,x4,x5,x6 } -> set means
  :Def4:
  x in it iff x=x1 or x=x2 or x =x3 or x=x4 or x=x5 or x=x6;
  existence
  proof
    take union({{x1,x2,x3,x4,x5},{x6}});
    let x;
    x in {x1,x2,x3,x4,x5} iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 by Def3;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

definition
  let x1,x2,x3,x4,x5,x6,x7;
  func { x1,x2,x3,x4,x5,x6,x7 } -> set means
  :Def5:
  x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7;
  existence
  proof
    take union({{x1,x2,x3,x4,x5,x6},{x7}});
    let x;
    x in { x1,x2,x3,x4,x5,x6 } iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or
    x=x6 by Def4;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6 or
    $1=x7;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

definition
  let x1,x2,x3,x4,x5,x6,x7,x8;
  func { x1,x2,x3,x4,x5,x6,x7,x8 } -> set means
  :Def6:
  x in it iff x=x1 or x= x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8;
  existence
  proof
    take union({{x1,x2,x3,x4,x5,x6,x7},{x8}});
    let x;
    x in { x1,x2,x3,x4,x5,x6,x7 } iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5
    or x = x6 or x=x7 by Def5;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6 or
    $1=x7 or $1=x8;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

definition
  let x1,x2,x3,x4,x5,x6,x7,x8,x9;
  func { x1,x2,x3,x4,x5,x6,x7,x8,x9 } -> set means
  :Def7:
  x in it iff x=x1 or
  x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9;
  existence
  proof
    take union({{x1,x2,x3,x4,x5,x6,x7,x8},{x9}});
    let x;
    x in { x1,x2,x3,x4,x5,x6,x7,x8 } iff x=x1 or x=x2 or x=x3 or x=x4 or x
    =x5 or x = x6 or x=x7 or x=x8 by Def6;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6 or
    $1=x7 or $1=x8 or $1=x9;
    thus for X, Y being set st (for x being set holds x in X iff P[x]) & (for
    x being set holds x in Y iff P[x]) holds X = Y from XBOOLE_0:sch 3;
  end;
end;

definition
  let x1,x2,x3,x4,x5,x6,x7,x8,x9,x10;
  func { x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 } -> set means
  :Def8:
  x in it iff x=x1
  or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9 or x=x10;
  existence
  proof
    take union({{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}});
    let x;
    x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } iff x=x1 or x=x2 or x=x3 or x=x4
    or x=x5 or x = x6 or x=x7 or x=x8 or x=x9 by Def7;
    hence thesis by Lm1;
  end;
  uniqueness
  proof
    defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6 or
    $1=x7 or $1=x8 or $1=x9 or $1=x10;
    thus for X, Y being set st (for x being set holds x in X iff P[x]) & (for
    x being set holds x in Y iff P[x]) holds X = Y from XBOOLE_0:sch 3;
  end;
end;

theorem Th1:
  { x1,x2 } = { x1 } \/ { x2 }
proof
  now
    let x;
    x in { x1,x2 } iff x=x1 or x=x2 by TARSKI:def 2;
    then x in { x1,x2 } iff x in { x1 } or x in { x2 } by TARSKI:def 1;
    hence x in { x1,x2 } iff x in { x1 } \/ { x2 } by XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th2:
  { x1,x2,x3 } = { x1 } \/ { x2,x3 }
proof
  now
    let x;
    x in { x1,x2,x3 } iff x=x1 or x=x2 or x=x3 by Def1;
    then x in { x1,x2,x3 } iff x in { x1 } or x in { x2,x3 } by TARSKI:def 1
,def 2;
    hence x in { x1,x2,x3 } iff x in { x1 } \/ { x2,x3 } by XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th3:
  { x1,x2,x3 } = { x1,x2 } \/ { x3 }
proof
  thus { x1,x2,x3 } = { x1 } \/ { x2,x3 } by Th2
    .= { x1 } \/ ({ x2 } \/ { x3 }) by Th1
    .= { x1 } \/ { x2 } \/ { x3 } by XBOOLE_1:4
    .= { x1,x2 } \/ { x3 } by Th1;
end;

Lm2: { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 }
proof
  now
    let x;
    x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4 by Def2;
    then x in { x1,x2,x3,x4 } iff x in { x1,x2 } or x in { x3,x4 } by
TARSKI:def 2;
    hence x in { x1,x2,x3,x4 } iff x in { x1,x2 } \/ { x3,x4 } by
XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th4:
  { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 }
proof
  thus { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm2
    .= { x1 } \/ { x2 } \/ { x3,x4 } by Th1
    .= { x1 } \/ ({ x2 } \/ { x3,x4 }) by XBOOLE_1:4
    .= { x1 } \/ { x2,x3,x4 } by Th2;
end;

theorem
  { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm2;

theorem Th6:
  { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 }
proof
  thus { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm2
    .= { x1,x2 } \/ ({ x3 } \/ { x4 }) by Th1
    .= { x1,x2 } \/ { x3 } \/ { x4 } by XBOOLE_1:4
    .= { x1,x2,x3 } \/ { x4 } by Th3;
end;

Lm3: { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 }
proof
  now
    let x;
    x in { x1,x2,x3,x4,x5 } iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 by Def3;
    then x in { x1,x2,x3,x4,x5 } iff x in { x1,x2,x3 } or x in { x4,x5 } by
Def1,TARSKI:def 2;
    hence x in { x1,x2,x3,x4,x5 } iff x in { x1,x2,x3 } \/ { x4,x5 } by
XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th7:
  { x1,x2,x3,x4,x5 } = { x1 } \/ { x2,x3,x4,x5 }
proof
  thus { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm3
    .= { x1 } \/ { x2,x3 } \/ { x4,x5 } by Th2
    .= { x1 } \/ ({ x2,x3 } \/ { x4,x5 }) by XBOOLE_1:4
    .= { x1 } \/ { x2,x3,x4,x5 } by Lm2;
end;

theorem Th8:
  { x1,x2,x3,x4,x5 } = { x1,x2 } \/ { x3,x4,x5 }
proof
  thus { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm3
    .= { x1,x2 } \/ { x3 } \/ { x4,x5 } by Th3
    .= { x1,x2 } \/ ({ x3 } \/ { x4,x5 }) by XBOOLE_1:4
    .= { x1,x2 } \/ { x3,x4,x5 } by Th2;
end;

theorem
  { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm3;

theorem Th10:
  { x1,x2,x3,x4,x5 } = { x1,x2,x3,x4 } \/ { x5 }
proof
  thus { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm3
    .= { x1,x2,x3 } \/ ({ x4 } \/ { x5 }) by Th1
    .= { x1,x2,x3 } \/ { x4 } \/ { x5 } by XBOOLE_1:4
    .= { x1,x2,x3,x4 } \/ { x5 } by Th6;
end;

Lm4: { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 }
proof
  now
    let x;
    x in { x1,x2,x3,x4,x5,x6 } iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or
    x=x6 by Def4;
    then
    x in { x1,x2,x3,x4,x5,x6 } iff x in { x1,x2,x3 } or x in { x4,x5,x6 }
    by Def1;
    hence x in { x1,x2,x3,x4,x5,x6 } iff x in { x1,x2,x3 } \/ { x4,x5,x6 } by
XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th11:
  { x1,x2,x3,x4,x5,x6 } = { x1 } \/ { x2,x3,x4,x5,x6 }
proof
  thus { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm4
    .= { x1 } \/ { x2,x3 } \/ { x4,x5,x6 } by Th2
    .= { x1 } \/ ({ x2,x3 } \/ { x4,x5,x6 }) by XBOOLE_1:4
    .= { x1 } \/ { x2,x3,x4,x5,x6 } by Th8;
end;

theorem Th12:
  { x1,x2,x3,x4,x5,x6 } = { x1,x2 } \/ { x3,x4,x5,x6 }
proof
  thus { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm4
    .= { x1,x2 } \/ { x3 } \/ { x4,x5,x6 } by Th3
    .= { x1,x2 } \/ ({ x3 } \/ { x4,x5,x6 }) by XBOOLE_1:4
    .= { x1,x2 } \/ { x3,x4,x5,x6 } by Th4;
end;

theorem
  { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm4;

theorem Th14:
  { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4 } \/ { x5,x6 }
proof
  thus { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm4
    .= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6 }) by Th2
    .= { x1,x2,x3 } \/ { x4 } \/ { x5,x6 } by XBOOLE_1:4
    .= { x1,x2,x3,x4 } \/ { x5,x6 } by Th6;
end;

theorem
  { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5 } \/ { x6 }
proof
  thus { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm4
    .= { x1,x2,x3 } \/ ({ x4,x5 } \/ { x6 }) by Th3
    .= { x1,x2,x3 } \/ { x4,x5 } \/ { x6 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5 } \/ { x6 } by Lm3;
end;

Lm5: { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 }
proof
  now
    let x;
A1: x in { x5,x6,x7 } iff x=x5 or x=x6 or x=x7 by Def1;
    x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4 by Def2;
    hence x in { x1,x2,x3,x4,x5,x6,x7 } iff x in { x1,x2,x3,x4 } \/ { x5,x6,x7
    } by A1,Def5,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th16:
  { x1,x2,x3,x4,x5,x6,x7 } = { x1 } \/ { x2,x3,x4,x5,x6,x7 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5
    .= { x1 } \/ { x2,x3,x4 } \/ { x5,x6,x7 } by Th4
    .= { x1 } \/ ({ x2,x3,x4 } \/ { x5,x6,x7 }) by XBOOLE_1:4
    .= { x1 } \/ { x2,x3,x4,x5,x6,x7 } by Lm4;
end;

theorem Th17:
  { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2 } \/ { x3,x4,x5,x6,x7 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5
    .= { x1,x2 } \/ { x3,x4 } \/ { x5,x6,x7 } by Lm2
    .= { x1,x2 } \/ ({ x3,x4 } \/ { x5,x6,x7 }) by XBOOLE_1:4
    .= { x1,x2 } \/ { x3,x4,x5,x6,x7 } by Th8;
end;

theorem Th18:
  { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3 } \/ { x4,x5,x6,x7 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5
    .= { x1,x2,x3 } \/ { x4 } \/ { x5,x6,x7 } by Th6
    .= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6,x7 }) by XBOOLE_1:4
    .= { x1,x2,x3 } \/ { x4,x5,x6,x7 } by Th4;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5;

theorem
  { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5 } \/ { x6,x7 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5
    .= { x1,x2,x3,x4 } \/ ({ x5 } \/ { x6,x7 }) by Th2
    .= { x1,x2,x3,x4 } \/ { x5 } \/ { x6,x7 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5 } \/ { x6,x7 } by Th10;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5,x6 } \/ { x7 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5
    .= { x1,x2,x3,x4 } \/ ({ x5,x6 } \/ { x7 }) by Th3
    .= { x1,x2,x3,x4 } \/ { x5,x6 } \/ { x7 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5,x6 } \/ { x7 } by Th14;
end;

Lm6: { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 }
proof
  now
    let x;
A1: x in { x5,x6,x7,x8 } iff x=x5 or x=x6 or x=x7 or x=x8 by Def2;
    x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4 by Def2;
    hence
    x in { x1,x2,x3,x4,x5,x6,x7,x8 } iff x in { x1,x2,x3,x4 } \/ { x5,x6,
    x7,x8 } by A1,Def6,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6
    .= { x1 } \/ { x2,x3,x4 } \/ { x5,x6,x7,x8 } by Th4
    .= { x1 } \/ ({ x2,x3,x4 } \/ { x5,x6,x7,x8 }) by XBOOLE_1:4
    .= { x1 } \/ { x2,x3,x4,x5,x6,x7,x8 } by Th18;
end;

theorem Th23:
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6
    .= { x1,x2 } \/ { x3,x4 } \/ { x5,x6,x7,x8 } by Lm2
    .= { x1,x2 } \/ ({ x3,x4 } \/ { x5,x6,x7,x8 }) by XBOOLE_1:4
    .= { x1,x2 } \/ { x3,x4,x5,x6,x7,x8 } by Th12;
end;

theorem Th24:
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6
    .= { x1,x2,x3 } \/ { x4 } \/ { x5,x6,x7,x8 } by Th6
    .= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6,x7,x8 }) by XBOOLE_1:4
    .= { x1,x2,x3 } \/ { x4,x5,x6,x7,x8 } by Th7;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6
    .= { x1,x2,x3,x4 } \/ ({x5 } \/ { x6,x7,x8 }) by Th4
    .= { x1,x2,x3,x4 } \/ {x5 } \/ { x6,x7,x8 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5 } \/ { x6,x7,x8 } by Th10;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6
    .= { x1,x2,x3,x4 } \/ ({ x5,x6 } \/ { x7,x8 }) by Lm2
    .= { x1,x2,x3,x4 } \/ { x5,x6 } \/ { x7,x8 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5,x6 } \/ { x7,x8 } by Th14;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6
    .= { x1,x2,x3,x4 } \/ ({ x5,x6,x7 } \/ { x8 }) by Th6
    .= { x1,x2,x3,x4 } \/ { x5,x6,x7 } \/ { x8 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5,x6,x7 } \/ { x8 } by Lm5;
end;

theorem Th29:
  { x1,x1 } = { x1 }
proof
  now
    let x;
    x in { x1,x1 } iff x = x1 by TARSKI:def 2;
    hence x in { x1,x1 } iff x in { x1 } by TARSKI:def 1;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th30:
  { x1,x1,x2 } = { x1,x2 }
proof
  thus { x1,x1,x2 } = { x1,x1 } \/ { x2 } by Th3
    .= { x1 } \/ { x2 } by Th29
    .= { x1,x2 } by Th1;
end;

theorem Th31:
  { x1,x1,x2,x3 } = { x1,x2,x3 }
proof
  thus { x1,x1,x2,x3 } = { x1,x1 } \/ { x2,x3 } by Lm2
    .= { x1 } \/ { x2,x3 } by Th29
    .= { x1,x2,x3 } by Th2;
end;

theorem Th32:
  { x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }
proof
  thus { x1,x1,x2,x3,x4 } = { x1,x1 } \/ { x2,x3,x4 } by Th8
    .= { x1 } \/ { x2,x3,x4 } by Th29
    .= { x1,x2,x3,x4 } by Th4;
end;

theorem Th33:
  { x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 }
proof
  thus { x1,x1,x2,x3,x4,x5 } = { x1,x1 } \/ { x2,x3,x4,x5 } by Th12
    .= { x1 } \/ { x2,x3,x4,x5 } by Th29
    .= { x1,x2,x3,x4,x5 } by Th7;
end;

theorem Th34:
  { x1,x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5,x6 }
proof
  thus { x1,x1,x2,x3,x4,x5,x6 } = { x1,x1 } \/ { x2,x3,x4,x5,x6 } by Th17
    .= { x1 } \/ { x2,x3,x4,x5,x6 } by Th29
    .= { x1,x2,x3,x4,x5,x6 } by Th11;
end;

theorem Th35:
  { x1,x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5,x6,x7 }
proof
  thus { x1,x1,x2,x3,x4,x5,x6,x7 } = { x1,x1 } \/ { x2,x3,x4,x5,x6,x7 } by Th23
    .= { x1 } \/ { x2,x3,x4,x5,x6,x7 } by Th29
    .= { x1,x2,x3,x4,x5,x6,x7 } by Th16;
end;

theorem
  { x1,x1,x1 } = { x1 }
proof
  thus { x1,x1,x1 } = { x1,x1 } by Th30
    .= { x1 } by Th29;
end;

theorem Th37:
  { x1,x1,x1,x2 } = { x1,x2 }
proof
  thus { x1,x1,x1,x2 } = { x1,x1,x2 } by Th31
    .= { x1,x2 } by Th30;
end;

theorem Th38:
  { x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
  thus { x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th32
    .= { x1,x2,x3 } by Th31;
end;

theorem Th39:
  { x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }
proof
  thus { x1,x1,x1,x2,x3,x4 } = { x1,x1,x2,x3,x4 } by Th33
    .= { x1,x2,x3,x4 } by Th32;
end;

theorem Th40:
  { x1,x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 }
proof
  thus { x1,x1,x1,x2,x3,x4,x5 } = { x1,x1,x2,x3,x4,x5 } by Th34
    .= { x1,x2,x3,x4,x5 } by Th33;
end;

theorem Th41:
  { x1,x1,x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5,x6 }
proof
  thus { x1,x1,x1,x2,x3,x4,x5,x6 } = { x1,x1,x2,x3,x4,x5,x6 } by Th35
    .= { x1,x2,x3,x4,x5,x6 } by Th34;
end;

theorem
  { x1,x1,x1,x1 } = { x1 }
proof
  thus { x1,x1,x1,x1 } = { x1,x1 } by Th37
    .= { x1 } by Th29;
end;

theorem Th43:
  { x1,x1,x1,x1,x2 } = { x1,x2 }
proof
  thus { x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th38
    .= { x1,x2 } by Th30;
end;

theorem Th44:
  { x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
  thus { x1,x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th39
    .= { x1,x2,x3 } by Th31;
end;

theorem Th45:
  { x1,x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }
proof
  thus { x1,x1,x1,x1,x2,x3,x4 } = { x1,x1,x2,x3,x4 } by Th40
    .= { x1,x2,x3,x4 } by Th32;
end;

theorem Th46:
  { x1,x1,x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 }
proof
  thus { x1,x1,x1,x1,x2,x3,x4,x5 } = { x1,x1,x2,x3,x4,x5 } by Th41
    .= { x1,x2,x3,x4,x5 } by Th33;
end;

theorem
  { x1,x1,x1,x1,x1 } = { x1 }
proof
  thus { x1,x1,x1,x1,x1 } = { x1,x1 } by Th43
    .= { x1 } by Th29;
end;

theorem Th48:
  { x1,x1,x1,x1,x1,x2 } = { x1,x2 }
proof
  thus { x1,x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th44
    .= { x1,x2 } by Th30;
end;

theorem Th49:
  { x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
  thus { x1,x1,x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th45
    .= { x1,x2,x3 } by Th31;
end;

theorem Th50:
  { x1,x1,x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }
proof
  thus { x1,x1,x1,x1,x1,x2,x3,x4 } = { x1,x1,x2,x3,x4 } by Th46
    .= { x1,x2,x3,x4 } by Th32;
end;

theorem
  { x1,x1,x1,x1,x1,x1 } = { x1 }
proof
  thus { x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th48
    .= { x1 } by Th29;
end;

theorem Th52:
  { x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 }
proof
  thus { x1,x1,x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th49
    .= { x1,x2 } by Th30;
end;

theorem Th53:
  { x1,x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
  thus { x1,x1,x1,x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th50
    .= { x1,x2,x3 } by Th31;
end;

theorem
  { x1,x1,x1,x1,x1,x1,x1 } = { x1 }
proof
  thus { x1,x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th52
    .= { x1 } by Th29;
end;

theorem Th55:
  { x1,x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 }
proof
  thus { x1,x1,x1,x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th53
    .= { x1,x2 } by Th30;
end;

theorem
  { x1,x1,x1,x1,x1,x1,x1,x1 } = { x1 }
proof
  thus { x1,x1,x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th55
    .= { x1 } by Th29;
end;

theorem Th57:
  { x1,x2,x3 } = { x1,x3,x2 }
proof
  thus { x1,x2,x3 } = { x1 } \/ { x2,x3 } by Th2
    .= { x1,x3,x2 } by Th2;
end;

theorem Th58:
  { x1,x2,x3 } = { x2,x1,x3 }
proof
  thus { x1,x2,x3 } = { x1,x2 } \/ { x3 } by Th3
    .= { x2,x1,x3 } by Th3;
end;

theorem Th59:
  { x1,x2,x3 } = { x2,x3,x1 }
proof
  thus { x1,x2,x3 } = { x2,x3 } \/ { x1 } by Th2
    .= { x2,x3,x1 } by Th3;
end;

theorem Th60:
  { x1,x2,x3 } = { x3,x2,x1 }
proof
  thus { x1,x2,x3 } = { x3,x1,x2 } by Th59
    .= { x3,x2,x1 } by Th57;
end;

theorem Th61:
  { x1,x2,x3,x4 } = { x1,x2,x4,x3 }
proof
  thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th4
    .= { x1 } \/ { x2,x4,x3 } by Th57
    .= { x1,x2,x4,x3 } by Th4;
end;

theorem
  { x1,x2,x3,x4 } = { x1,x3,x2,x4 }
proof
  thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th4
    .= { x1 } \/ { x3,x2,x4 } by Th58
    .= { x1,x3,x2,x4 } by Th4;
end;

theorem Th63:
  { x1,x2,x3,x4 } = { x1,x3,x4,x2 }
proof
  thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th4
    .= { x1 } \/ { x3,x4,x2 } by Th59
    .= { x1,x3,x4,x2 } by Th4;
end;

theorem Th64:
  { x1,x2,x3,x4 } = { x1,x4,x3,x2 }
proof
  thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th4
    .= { x1 } \/ { x4,x3,x2 } by Th60
    .= { x1,x4,x3,x2 } by Th4;
end;

theorem Th65:
  { x1,x2,x3,x4 } = { x2,x1,x3,x4 }
proof
  thus { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 } by Th6
    .= { x2,x1,x3 } \/ { x4 } by Th58
    .= { x2,x1,x3,x4 } by Th6;
end;

Lm7: { x1,x2,x3,x4 } = { x2,x3,x1,x4 }
proof
  thus { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 } by Th6
    .= { x2,x3,x1 } \/ { x4 } by Th59
    .= { x2,x3,x1,x4 } by Th6;
end;

theorem
  { x1,x2,x3,x4 } = { x2,x1,x4,x3 }
proof
  thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm7
    .= { x2,x1,x4,x3 } by Th63;
end;

theorem
  { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm7;

theorem
  { x1,x2,x3,x4 } = { x2,x3,x4,x1 }
proof
  thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm7
    .= { x2,x3,x4,x1 } by Th61;
end;

theorem Th69:
  { x1,x2,x3,x4 } = { x2,x4,x1,x3 }
proof
  thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm7
    .= { x2,x4,x1,x3 } by Th64;
end;

theorem
  { x1,x2,x3,x4 } = { x2,x4,x3,x1 }
proof
  thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm7
    .= { x2,x4,x3,x1 } by Th63;
end;

Lm8: { x1,x2,x3,x4 } = { x3,x2,x1,x4 }
proof
  thus { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 } by Th6
    .= { x3,x2,x1 } \/ { x4 } by Th60
    .= { x3,x2,x1,x4 } by Th6;
end;

theorem
  { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm8;

theorem
  { x1,x2,x3,x4 } = { x3,x2,x4,x1 }
proof
  thus { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm8
    .= { x3,x2,x4,x1 } by Th61;
end;

theorem
  { x1,x2,x3,x4 } = { x3,x4,x1,x2 }
proof
  thus { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm8
    .= { x3,x4,x1,x2 } by Th64;
end;

theorem Th74:
  { x1,x2,x3,x4 } = { x3,x4,x2,x1 }
proof
  thus { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm8
    .= { x3,x4,x2,x1 } by Th63;
end;

theorem
  { x1,x2,x3,x4 } = { x4,x2,x3,x1 }
proof
  thus { x1,x2,x3,x4 } = { x3,x4,x2,x1 } by Th74
    .= { x4,x2,x3,x1 } by Lm7;
end;

theorem
  { x1,x2,x3,x4 } = { x4,x3,x2,x1 }
proof
  thus { x1,x2,x3,x4 } = { x3,x4,x2,x1 } by Th74
    .= { x4,x3,x2,x1 } by Th65;
end;

Lm9: { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
proof
  now
    let x;
A1: x in { x5,x6,x7,x8,x9 } iff x=x5 or x=x6 or x=x7 or x=x8 or x=x9 by Def3;
    x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4 by Def2;
    hence
    x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } iff x in { x1,x2,x3,x4 } \/ { x5,
    x6,x7,x8,x9 } by A1,Def7,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8,x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= ({ x1 } \/ { x2,x3,x4 }) \/ { x5,x6,x7,x8,x9 } by Th4
    .= { x1 } \/ ({ x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }) by XBOOLE_1:4
    .= { x1 } \/ { x2,x3,x4,x5,x6,x7,x8,x9 } by Th24;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8,x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= { x1,x2 } \/ { x3,x4 } \/ { x5,x6,x7,x8,x9 } by Lm2
    .= { x1,x2 } \/ ({ x3,x4 } \/ { x5,x6,x7,x8,x9 }) by XBOOLE_1:4
    .= { x1,x2 } \/ { x3,x4,x5,x6,x7,x8,x9 } by Th17;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8,x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= { x1,x2,x3 } \/ { x4 } \/ { x5,x6,x7,x8,x9 } by Th6
    .= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6,x7,x8,x9 }) by XBOOLE_1:4
    .= { x1,x2,x3 } \/ { x4,x5,x6,x7,x8,x9 } by Th11;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8,x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= { x1,x2,x3,x4 } \/ ({x5 } \/ { x6,x7,x8,x9 }) by Th7
    .= { x1,x2,x3,x4 } \/ {x5 } \/ { x6,x7,x8,x9 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5 } \/ { x6,x7,x8,x9 } by Th10;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8,x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= { x1,x2,x3,x4 } \/ ({ x5,x6 } \/ { x7,x8,x9 }) by Th8
    .= { x1,x2,x3,x4 } \/ { x5,x6 } \/ { x7,x8,x9 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5,x6 } \/ { x7,x8,x9 } by Th14;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8,x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= { x1,x2,x3,x4 } \/ ({ x5,x6,x7 } \/ { x8,x9 }) by Lm3
    .= { x1,x2,x3,x4 } \/ { x5,x6,x7 } \/ { x8,x9 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5,x6,x7 } \/ { x8,x9 } by Lm5;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7,x8 } \/ { x9 }
proof
  thus { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
  by Lm9
    .= { x1,x2,x3,x4 } \/ ({ x5,x6,x7,x8 } \/ { x9 }) by Th10
    .= { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } \/ { x9 } by XBOOLE_1:4
    .= { x1,x2,x3,x4,x5,x6,x7,x8 } \/ { x9 } by Lm6;
end;

theorem
  { x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 } = { x1,x2,x3,x4,x5,x6,x7,x8,x9 } \/
  { x10 }
proof
  now
    let x;
A1: x in {x10} iff x=x10 by TARSKI:def 1;
    x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9
    or x=x10 iff x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } or x = x10 by Def7;
    hence
    x in { x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 } iff x in { x1,x2,x3,x4,x5,x6,
    x7,x8,x9 } \/ {x10} by A1,Def8,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

begin :: Addenda

theorem :: from AMI_7, 2006.03.15, A.T.
  for x, y, z being set st x <> y & x <> z holds {x, y, z} \ {x} = {y, z }
proof
  let x, y, z be set such that
A1: x <> y & x <> z;
  hereby
    let a be set;
    assume
A2: a in {x, y, z} \ {x};
    then a in {x, y, z} by XBOOLE_0:def 5;
    then
A3: a = x or a = y or a = z by Def1;
    not a in {x} by A2,XBOOLE_0:def 5;
    hence a in {y, z} by A3,TARSKI:def 1,def 2;
  end;
  let a be set;
  assume a in {y, z};
  then
A4: a = y or a = z by TARSKI:def 2;
  then
A5: not a in {x} by A1,TARSKI:def 1;
  a in {x, y, z} by A4,Def1;
  hence thesis by A5,XBOOLE_0:def 5;
end;

:: from SCMBSORT, 2007.07.26, A.T.

theorem
  for x1,x2,x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3}
proof
  let x1,x2,x3 be set;
  thus {x2,x1} \/ {x3,x1} = {x2,x1,x3,x1} by Lm2
    .= {x1,x1,x2,x3} by Th69
    .= {x1,x2,x3} by Th31;
end;