PZFMISC1

:: Some Basic Properties of Many Sorted Sets
::  by Artur Korni{\l}owicz
::
:: Received September 29, 1995
:: Copyright (c) 1995-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 FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, FINSET_1,
      TARSKI, ZFMISC_1, PZFMISC1, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1,
      FUNCOP_1, PBOOLE, MBOOLEAN;
 constructors FUNCT_4, MBOOLEAN, PBOOLE, FINSET_1, RELSET_1;
 registrations XBOOLE_0, FUNCOP_1, FINSET_1;
 requirements BOOLE;
 definitions FINSET_1, PBOOLE;
 equalities FUNCOP_1;
 expansions PBOOLE;
 theorems FUNCOP_1, ENUMSET1, FUNCT_4, MBOOLEAN, PBOOLE, TARSKI, ZFMISC_1,
      RELAT_1, XBOOLE_0, PARTFUN1;
 schemes PBOOLE;

begin :: Preliminaries

reserve i for object, I for set,
  f for Function,
  x, x1, x2, y, A, B, X, Y, Z for ManySortedSet of I;

theorem Th1:
  for X be object for M be ManySortedSet of I st i in I
  holds dom (M +* (i .--> X)) = I
proof
  let X be object, M be ManySortedSet of I such that
A1: i in I;
  thus dom (M +* (i .--> X)) = dom M \/ dom (i .--> X) by FUNCT_4:def 1
    .= I \/ dom (i .--> X) by PARTFUN1:def 2
    .= I \/ {i}
    .= I by A1,ZFMISC_1:40;
end;

theorem
  f = {} implies f is ManySortedSet of {} by PARTFUN1:def 2,RELAT_1:38,def 18;

theorem
  I is non empty implies not ex X st X is empty-yielding & X is non-empty
proof
  assume
A1: I is non empty;
  given X such that
A2: X is empty-yielding and
A3: X is non-empty;
  consider i being object such that
A4: i in I by A1,XBOOLE_0:def 1;
  X.i is empty by A2,A4;
  hence contradiction by A3,A4;
end;

begin :: Singelton and unordered pairs

definition
  let I, A;
  func {A} -> ManySortedSet of I means
  :Def1:
  for i being object st i in I holds it.i = {A.i};
  existence
  proof
    deffunc F(object) = {A.$1};
    thus ex M be ManySortedSet of I st for i st i in I holds M.i = F(i)
    from PBOOLE:sch 4;
  end;
  uniqueness
  proof
    let X, Y be ManySortedSet of I such that
A1: for i being object st i in I holds X.i = {A.i} and
A2: for i being object st i in I holds Y.i = {A.i};
    now
      let i be object;
      assume
A3:   i in I;
      hence X.i = {A.i} by A1
        .= Y.i by A2,A3;
    end;
    hence X = Y;
  end;
end;

registration
  let I, A;
  cluster {A} -> non-empty finite-yielding;
  coherence
  proof
    thus {A} is non-empty
    proof
      let i be object such that
A1:   i in I;
      {A.i} <> {};
      hence thesis by A1,Def1;
    end;
    let i be object such that
A2: i in I;
    {A.i} is finite;
    hence thesis by A2,Def1;
  end;
end;

definition
  let I, A, B;
  func {A,B} -> ManySortedSet of I means
  :Def2:
  for i being object st i in I holds it.i = {A.i,B.i};
  existence
  proof
    deffunc F(object) = {A.$1,B.$1};
    thus ex M be ManySortedSet of I st
   for i being object st i in I holds M.i = F(i)
    from PBOOLE:sch 4;
  end;
  uniqueness
  proof
    let X, Y be ManySortedSet of I such that
A1: for i being object st i in I holds X.i = {A.i,B.i} and
A2: for i being object st i in I holds Y.i = {A.i,B.i};
    now
      let i be object;
      assume
A3:   i in I;
      hence X.i = {A.i,B.i} by A1
        .= Y.i by A2,A3;
    end;
    hence X = Y;
  end;
  commutativity;
end;

registration
  let I, A, B;
  cluster {A,B} -> non-empty finite-yielding;
  coherence
  proof
    thus {A,B} is non-empty
    proof
      let i be object such that
A1:   i in I;
      {A.i,B.i} <> {};
      hence thesis by A1,Def2;
    end;
    let i being object such that
A2: i in I;
    {A.i,B.i} is finite;
    hence thesis by A2,Def2;
  end;
end;

theorem     :: Tarski:3
  X = { y } iff for x holds x in X iff x = y
proof
  thus X = { y } implies for x holds x in X iff x = y
  proof
    assume
A1: X = {y};
    let x;
    thus x in X implies x = y
    proof
      assume
A2:   x in X;
      now
        let i be object;
        assume
A3:     i in I;
        then
A4:     x.i in X.i by A2;
        X.i = {y.i} by A1,A3,Def1;
        hence x.i = y.i by A4,TARSKI:def 1;
      end;
      hence thesis;
    end;
    assume
A5: x = y;
    let i be object;
    assume i in I;
    then X.i = {y.i} by A1,Def1;
    hence thesis by A5,TARSKI:def 1;
  end;
  assume
A6: for x holds x in X iff x = y;
  then
A7: y in X;
  now
    let i be object such that
A8: i in I;
    now
      let a be object;
      thus a in X.i iff a = y.i
      proof
        thus a in X.i implies a = y.i
        proof
          assume
A9:       a in X.i;
A10:      dom (i .--> a) = {i};
          dom (y +* (i .--> a)) = I by A8,Th1;
          then reconsider x1 = y +* (i .--> a) as ManySortedSet of I
          by PARTFUN1:def 2,RELAT_1:def 18;
          i in {i} by TARSKI:def 1;
          then
A11:      x1.i = (i .--> a).i by A10,FUNCT_4:13
            .= a by FUNCOP_1:72;
          x1 in X
          proof
            let q be object such that
A12:        q in I;
            per cases;
            suppose i = q;
              hence thesis by A9,A11;
            end;
            suppose i <> q;
              then not q in dom (i .--> a) by TARSKI:def 1;
              then x1.q = y.q by FUNCT_4:11;
              hence thesis by A7,A12;
            end;
          end;
          hence thesis by A6,A11;
        end;
        assume a = y.i;
        hence thesis by A7,A8;
      end;
    end;
    then X.i = {y.i} by TARSKI:def 1;
    hence X.i = {y}.i by A8,Def1;
  end;
  hence thesis;
end;

theorem     :: Tarski:4 a
  (for x holds x in X iff x = x1 or x = x2) implies X = { x1,x2 }
proof
  assume
A1: for x holds x in X iff x = x1 or x = x2;
  then
A2: x1 in X;
A3: x2 in X by A1;
  now
    let i be object such that
A4: i in I;
    now
      let a be object;
      thus a in X.i iff a = x1.i or a = x2.i
      proof
        thus a in X.i implies a = x1.i or a = x2.i
        proof
          assume that
A5:       a in X.i and
A6:       a <> x1.i;
A7:       dom (i .--> a) = {i};
          dom (x2 +* (i .--> a)) = I by A4,Th1;
          then reconsider k2 = x2 +* (i .--> a) as ManySortedSet of I
          by PARTFUN1:def 2,RELAT_1:def 18;
          i in {i} by TARSKI:def 1;
          then
A8:       k2.i = (i .--> a).i by A7,FUNCT_4:13
            .= a by FUNCOP_1:72;
          k2 in X
          proof
            let q be object such that
A9:         q in I;
            per cases;
            suppose i = q;
              hence thesis by A5,A8;
            end;
            suppose i <> q;
              then not q in dom (i .--> a) by TARSKI:def 1;
              then k2.q = x2.q by FUNCT_4:11;
              hence thesis by A3,A9;
            end;
          end;
          hence thesis by A1,A6,A8;
        end;
        assume
A10:    a = x1.i or a = x2.i;
        per cases by A10;
        suppose a = x1.i;
          hence thesis by A2,A4;
        end;
        suppose a = x2.i;
          hence thesis by A3,A4;
        end;
      end;
    end;
    then X.i = {x1.i,x2.i} by TARSKI:def 2;
    hence X.i = { x1,x2 }.i by A4,Def2;
  end;
  hence thesis;
end;

theorem     :: Tarski:4 b
  X = { x1,x2 } implies for x holds x = x1 or x = x2 implies x in X
proof
  assume
A1: X = { x1,x2 };
  let x;
  assume
A2: x = x1 or x = x2;
  let i;
  assume i in I;
  then
A3: X.i = {x1.i,x2.i} by A1,Def2;
  per cases by A2;
  suppose x = x1;
    hence thesis by A3,TARSKI:def 2;
  end;
  suppose x = x2;
    hence thesis by A3,TARSKI:def 2;
  end;
end;

theorem     :: ENUMSET1:3
  x in { A } implies x = A
proof
  assume
A1: x in { A };
  now
    let i be object;
    assume
A2: i in I;
    then x.i in {A}.i by A1;
    then x.i in {A.i} by A2,Def1;
    hence x.i = A.i by TARSKI:def 1;
  end;
  hence thesis;
end;

theorem     :: ENUMSET1:4
  x in { x }
proof
  let i such that
A1: i in I;
  x.i in {x.i} by TARSKI:def 1;
  hence thesis by A1,Def1;
end;

theorem     :: ENUMSET1:9
  x = A or x = B implies x in { A,B }
proof
  assume
A1: x=A or x=B;
  per cases by A1;
  suppose
A2: x=A;
    let i such that
A3: i in I;
    x.i in {A.i,B.i} by A2,TARSKI:def 2;
    hence thesis by A3,Def2;
  end;
  suppose
A4: x=B;
    let i such that
A5: i in I;
    x.i in {A.i,B.i} by A4,TARSKI:def 2;
    hence thesis by A5,Def2;
  end;
end;

theorem     ::ENUMSET1:41
  {A} (\/) {B} = {A,B}
proof
  now
    let i be object;
    assume
A1: i in I;
    hence ({A} (\/) {B}).i = {A}.i \/ {B}.i by PBOOLE:def 4
      .= {A}.i \/ {B.i} by A1,Def1
      .= {A.i} \/ {B.i} by A1,Def1
      .= {A.i,B.i} by ENUMSET1:1
      .= {A,B}.i by A1,Def2;
  end;
  hence thesis;
end;

theorem     :: ENUMSET1:69
  { x,x } = { x }
proof
  now
    let i be object;
    assume
A1: i in I;
    hence { x,x }.i = {x.i,x.i} by Def2
      .= {x.i} by ENUMSET1:29
      .= { x }.i by A1,Def1;
  end;
  hence thesis;
end;

theorem     :: SETWISEO:1
  {A} c= {B} implies A = B
proof
  assume
A1: {A} c= {B};
  now
    let i be object;
    assume
A2: i in I;
    then {A}.i c= {B}.i by A1;
    then {A}.i c= {B.i} by A2,Def1;
    then {A.i} c= {B.i} by A2,Def1;
    hence A.i = B.i by ZFMISC_1:18;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:6
  {x} = {y} implies x = y
proof
  assume
A1: {x} = {y};
  now
    let i be object;
    assume
A2: i in I;
    then {x.i} = {x}.i by Def1
      .= {y.i} by A1,A2,Def1;
    hence x.i = y.i by ZFMISC_1:3;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:8
  {x} = {A,B} implies x = A & x = B
proof
  assume
A1: {x} = {A,B};
  now
    let i be object;
    assume
A2: i in I;
    then {x.i} = {x}.i by Def1
      .= {A.i,B.i} by A1,A2,Def2;
    hence x.i = A.i by ZFMISC_1:4;
  end;
  hence x = A;
  now
    let i be object;
    assume
A3: i in I;
    then {x.i} = {x}.i by Def1
      .= {A.i,B.i} by A1,A3,Def2;
    hence x.i = B.i by ZFMISC_1:4;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:9
  {x} = {A,B} implies A = B
proof
  assume
A1: {x} = {A,B};
  now
    let i be object;
    assume
A2: i in I;
    then {x.i} = {x}.i by Def1
      .= {A.i,B.i} by A1,A2,Def2;
    hence A.i = B.i by ZFMISC_1:5;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:12
  {x} c= {x,y} & {y} c= {x,y}
proof
  thus {x} c= {x,y}
  proof
    let i such that
A1: i in I;
    {x.i} c= {x.i,y.i} by ZFMISC_1:7;
    then {x}.i c= {x.i,y.i} by A1,Def1;
    hence thesis by A1,Def2;
  end;
  let i such that
A2: i in I;
  {y.i} c= {x.i,y.i} by ZFMISC_1:7;
  then {y}.i c= {x.i,y.i} by A2,Def1;
  hence thesis by A2,Def2;
end;

theorem     :: ZFMISC_1:13
  {x} (\/) {y} = {x} implies x = y
proof
  assume
A1: {x} (\/) {y} = {x};
  now
    let i be object such that
A2: i in I;
      {x.i} \/ {y.i} = {x.i} \/ {y}.i by A2,Def1
        .= {x}.i \/ {y}.i by A2,Def1
        .= ({x} (\/) {y}).i by A2,PBOOLE:def 4
        .= {x.i} by A2,A1,Def1;
      hence x.i = y.i by ZFMISC_1:8;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:14
  {x} (\/) {x,y} = {x,y}
proof
  now
    let i be object;
    assume
A1: i in I;
    hence ({x} (\/) {x,y}).i = {x}.i \/ {x,y}.i by PBOOLE:def 4
      .= {x.i} \/ {x,y}.i by A1,Def1
      .= {x.i} \/ {x.i,y.i} by A1,Def2
      .= {x.i,y.i} by ZFMISC_1:9
      .= {x,y}.i by A1,Def2;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:16
  I is non empty & {x} (/\) {y} = EmptyMS I implies x <> y
proof
  assume that
A1: I is non empty and
A2: {x} (/\) {y} = EmptyMS I;
  now
    consider i being object such that
A3: i in I by A1,XBOOLE_0:def 1;
    take i;
    {x.i} /\ {y.i} = {x}.i /\ {y.i} by A3,Def1
      .= {x}.i /\ {y}.i by A3,Def1
      .= ({x} (/\) {y}).i by A3,PBOOLE:def 5
      .= {} by A2,PBOOLE:5;
    hence x.i <> y.i;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:18
  {x} (/\) {y} = {x} implies x = y
proof
  assume
A1: {x} (/\) {y} = {x};
    now
      let i be object;
      assume
A2:   i in I;
      then {x.i} /\ {y.i} = {x.i} /\ {y}.i by Def1
        .= {x}.i /\ {y}.i by A2,Def1
        .= ({x} (/\) {y}).i by A2,PBOOLE:def 5
        .= {x.i} by A1,A2,Def1;
      hence x.i = y.i by ZFMISC_1:12;
    end;
    hence thesis;
end;

theorem     :: ZFMISC_1:19
  {x} (/\) {x,y} = {x}
proof
  now
    let i be object;
    assume
A1: i in I;
    hence ({x} (/\) {x,y}).i = {x}.i /\ {x,y}.i by PBOOLE:def 5
      .= {x.i} /\ {x,y}.i by A1,Def1
      .= {x.i} /\ {x.i,y.i} by A1,Def2
      .= {x.i} by ZFMISC_1:13
      .= {x}.i by A1,Def1;
  end;
  hence {x} (/\) {x,y} = {x};
end;

theorem     :: ZFMISC_1:20
  I is non empty & {x} (\) {y} = {x} implies x <> y
proof
  assume that
A1: I is non empty and
A2: {x} (\) {y} = {x};
  now
    consider i being object such that
A3: i in I by A1,XBOOLE_0:def 1;
    take i;
    {x.i} \ {y.i} = {x}.i \ {y.i} by A3,Def1
      .= {x}.i \ {y}.i by A3,Def1
      .= ({x} (\) {y}).i by A3,PBOOLE:def 6
      .= {x.i} by A2,A3,Def1;
    hence x.i <> y.i by ZFMISC_1:14;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:21
  {x} (\) {y} = EmptyMS I implies x = y
proof
  assume
A1: {x} (\) {y} = EmptyMS I;
  now
    let i be object;
    assume
A2: i in I;
    then {x.i} \ {y.i} = {x}.i \ {y.i} by Def1
      .= {x}.i \ {y}.i by A2,Def1
      .= ({x} (\) {y}).i by A2,PBOOLE:def 6
      .= {} by A1,PBOOLE:5;
    hence x.i = y.i by ZFMISC_1:15;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:22
  {x} (\) {x,y} = EmptyMS I
proof
  now
    let i be object;
    assume
A1: i in I;
    hence ({x} (\) {x,y}).i = {x}.i \ {x,y}.i by PBOOLE:def 6
      .= {x.i} \ {x,y}.i by A1,Def1
      .= {x.i} \ {x.i,y.i} by A1,Def2
      .= {} by ZFMISC_1:16
      .= EmptyMS I.i by PBOOLE:5;
  end;
  hence {x} (\) {x,y} = EmptyMS I;
end;

theorem     :: ZFMISC_1:24
  {x} c= {y} implies {x} = {y}
proof
  assume
A1: {x} c= {y};
  now
    let i be object;
    assume
A2: i in I;
    then {x}.i c= {y}.i by A1;
    then {x.i} c= {y}.i by A2,Def1;
    then
A3: {x.i} c= {y.i} by A2,Def1;
    thus {x}.i = {x.i} by A2,Def1
      .= {y.i} by A3,ZFMISC_1:18
      .= {y}.i by A2,Def1;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:26
  {x,y} c= {A} implies x = A & y = A
proof
  assume
A1: {x,y} c= {A};
  now
    let i be object;
    assume
A2: i in I;
    then {x,y}.i c= {A}.i by A1;
    then {x,y}.i c= {A.i} by A2,Def1;
    then {x.i,y.i} c= {A.i} by A2,Def2;
    hence x.i = A.i by ZFMISC_1:20;
  end;
  hence x = A;
  now
    let i be object;
    assume
A3: i in I;
    then {x,y}.i c= {A}.i by A1;
    then {x,y}.i c= {A.i} by A3,Def1;
    then {x.i,y.i} c= {A.i} by A3,Def2;
    hence y.i = A.i by ZFMISC_1:20;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:27
  {x,y} c= {A} implies {x,y} = {A}
proof
  assume
A1: {x,y} c= {A};
  now
    let i be object;
    assume
A2: i in I;
    then {x,y}.i c= {A}.i by A1;
    then {x.i,y.i} c= {A}.i by A2,Def2;
    then
A3: {x.i,y.i} c= {A.i} by A2,Def1;
    thus {x,y}.i = {x.i,y.i} by A2,Def2
      .= {A.i} by A3,ZFMISC_1:21
      .= {A}.i by A2,Def1;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:30
  bool { x } = { EmptyMS I, {x} }
proof
  now
    let i be object;
    assume
A1: i in I;
    hence (bool {x}).i = bool ({x}.i) by MBOOLEAN:def 1
      .= bool ({x.i}) by A1,Def1
      .= {{}, {x.i}} by ZFMISC_1:24
      .= {EmptyMS I.i, {x.i}} by PBOOLE:5
      .= {EmptyMS I.i, {x}.i} by A1,Def1
      .= { EmptyMS I, {x} }.i by A1,Def2;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:80
  { A } c= bool A
proof
  let i such that
A1: i in I;
  {A.i} c= bool (A.i) by ZFMISC_1:68;
  then {A}.i c= bool (A.i) by A1,Def1;
  hence thesis by A1,MBOOLEAN:def 1;
end;

theorem     :: ZFMISC_1:31
  union { x } = x
proof
  now
    let i be object;
    assume
A1: i in I;
    hence (union { x }).i = union ({x}.i) by MBOOLEAN:def 2
      .= union {x.i} by A1,Def1
      .= x.i by ZFMISC_1:25;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:32
  union { {x},{y} } = {x,y}
proof
  now
    let i be object;
    assume
A1: i in I;
    hence (union { {x},{y} }).i = union ({{x},{y}}.i) by MBOOLEAN:def 2
      .= union {{x}.i,{y}.i} by A1,Def2
      .= union {{x.i},{y}.i} by A1,Def1
      .= union {{x.i},{y.i}} by A1,Def1
      .= {x.i,y.i} by ZFMISC_1:26
      .= {x,y}.i by A1,Def2;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:93
  union { A,B } = A (\/) B
proof
  now
    let i be object;
    assume
A1: i in I;
    hence (union { A,B }).i = union ({A,B}.i) by MBOOLEAN:def 2
      .= union {A.i,B.i} by A1,Def2
      .= A.i \/ B.i by ZFMISC_1:75
      .= (A (\/) B).i by A1,PBOOLE:def 4;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:37
  {x} c= X iff x in X
proof
  thus {x} c= X implies x in X
  proof
    assume
A1: {x} c= X;
    let i;
    assume
A2: i in I;
    then {x}.i c= X.i by A1;
    then {x.i} c= X.i by A2,Def1;
    hence thesis by ZFMISC_1:31;
  end;
  assume
A3: x in X;
  let i;
  assume
A4: i in I;
  then x.i in X.i by A3;
  then {x.i} c= X.i by ZFMISC_1:31;
  hence thesis by A4,Def1;
end;

theorem     :: ZFMISC_1:38
  {x1,x2} c= X iff x1 in X & x2 in X
proof
  thus {x1,x2} c= X implies x1 in X & x2 in X
  proof
    assume
A1: {x1,x2} c= X;
    thus x1 in X
    proof
      let i;
      assume
A2:   i in I;
      then {x1,x2}.i c= X.i by A1;
      then {x1.i,x2.i} c= X.i by A2,Def2;
      hence thesis by ZFMISC_1:32;
    end;
    let i;
    assume
A3: i in I;
    then {x1,x2}.i c= X.i by A1;
    then {x1.i,x2.i} c= X.i by A3,Def2;
    hence thesis by ZFMISC_1:32;
  end;
  assume that
A4: x1 in X and
A5: x2 in X;
  let i;
  assume
A6: i in I;
  then
A7: x1.i in X.i by A4;
  x2.i in X.i by A5,A6;
  then {x1.i,x2.i} c= X.i by A7,ZFMISC_1:32;
  hence thesis by A6,Def2;
end;

theorem     :: ZFMISC_1:42
  A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} implies A c= {x1,x2}
proof
  assume
A1: A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2};
  let i such that
A2: i in I;
  per cases by A1;
  suppose A = EmptyMS I;
    then A.i = {} by PBOOLE:5;
    then A.i c= {x1.i,x2.i} by ZFMISC_1:36;
    hence thesis by A2,Def2;
  end;
  suppose A = {x1};
    then A.i = {x1.i} by A2,Def1;
    then A.i c= {x1.i,x2.i} by ZFMISC_1:36;
    hence thesis by A2,Def2;
  end;
  suppose A = {x2};
    then A.i = {x2.i} by A2,Def1;
    then A.i c= {x1.i,x2.i} by ZFMISC_1:36;
    hence thesis by A2,Def2;
  end;
  suppose A = {x1,x2};
    hence thesis;
  end;
end;

begin :: Sum of an unordered pairs (or a singelton) and a set

theorem     :: SETWISEO:6
  x in A or x = B implies x in A (\/) {B}
proof
  assume
A1: x in A or x = B;
  let i such that
A2: i in I;
  per cases by A1;
  suppose x in A;
    then x.i in A.i by A2;
    then x.i in A.i \/ {B.i} by ZFMISC_1:136;
    then x.i in A.i \/ {B}.i by A2,Def1;
    hence thesis by A2,PBOOLE:def 4;
  end;
  suppose x = B;
    then x.i in A.i \/ {B.i} by ZFMISC_1:136;
    then x.i in A.i \/ {B}.i by A2,Def1;
    hence thesis by A2,PBOOLE:def 4;
  end;
end;

theorem     :: SETWISEO:8
  A (\/) {x} c= B iff x in B & A c= B
proof
  thus A (\/) {x} c= B implies x in B & A c= B
  proof
    assume
A1: A (\/) {x} c= B;
A2: now
      let i;
      assume
A3:   i in I;
      then (A (\/) {x}).i c= B.i by A1;
      then A.i \/ {x}.i c= B.i by A3,PBOOLE:def 4;
      hence A.i \/ {x.i} c= B.i by A3,Def1;
    end;
    thus x in B
    proof
      let i;
      assume i in I;
      then A.i \/ {x.i} c= B.i by A2;
      hence thesis by ZFMISC_1:137;
    end;
    let i;
    assume i in I;
    then A.i \/ {x.i} c= B.i by A2;
    hence thesis by ZFMISC_1:137;
  end;
  assume that
A4: x in B and
A5: A c= B;
  let i;
  assume
A6: i in I;
  then
A7: x.i in B.i by A4;
  A.i c= B.i by A5,A6;
  then A.i \/ {x.i} c= B.i by A7,ZFMISC_1:137;
  then A.i \/ {x}.i c= B.i by A6,Def1;
  hence thesis by A6,PBOOLE:def 4;
end;

theorem     :: ZFMISC_1:45
  {x} (\/) X = X implies x in X
proof
  assume
A1: {x} (\/) X = X;
  let i;
  assume
A2: i in I;
  then {x.i} \/ X.i = {x}.i \/ X.i by Def1
    .= X.i by A1,A2,PBOOLE:def 4;
  hence thesis by ZFMISC_1:39;
end;

theorem     :: ZFMISC_1:46
  x in X implies {x} (\/) X = X
proof
  assume
A1: x in X;
  now
    let i be object;
    assume
A2: i in I;
    then
A3: x.i in X.i by A1;
    thus ({x} (\/) X).i = {x}.i \/ X.i by A2,PBOOLE:def 4
      .= {x.i} \/ X.i by A2,Def1
      .= X.i by A3,ZFMISC_1:40;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:47, 48
  {x,y} (\/) A = A iff x in A & y in A
proof
  thus {x,y} (\/) A = A implies x in A & y in A
  proof
    assume
A1: {x,y} (\/) A = A;
    thus x in A
    proof
      let i;
      assume
A2:   i in I;
      then {x.i,y.i} \/ A.i = {x,y}.i \/ A.i by Def2
        .= A.i by A1,A2,PBOOLE:def 4;
      hence thesis by ZFMISC_1:41;
    end;
    let i;
    assume
A3: i in I;
    then {x.i,y.i} \/ A.i = {x,y}.i \/ A.i by Def2
      .= A.i by A1,A3,PBOOLE:def 4;
    hence thesis by ZFMISC_1:41;
  end;
  assume that
A4: x in A and
A5: y in A;
  now
    let i be object;
    assume
A6: i in I;
    then
A7: x.i in A.i by A4;
A8: y.i in A.i by A5,A6;
    thus ({x,y} (\/) A).i = {x,y}.i \/ A.i by A6,PBOOLE:def 4
      .= {x.i,y.i} \/ A.i by A6,Def2
      .= A.i by A7,A8,ZFMISC_1:42;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:49
  I is non empty implies {x} (\/) X <> EmptyMS I
proof
  assume that
A1: I is non empty and
A2: {x} (\/) X = EmptyMS I;
  consider i being object such that
A3: i in I by A1,XBOOLE_0:def 1;
  {x.i} \/ X.i <> {};
  then {x}.i \/ X.i <> {} by A3,Def1;
  then ({x} (\/) X).i <> {} by A3,PBOOLE:def 4;
  hence contradiction by A2,PBOOLE:5;
end;

theorem     :: ZFMISC_1:50
  I is non empty implies {x,y} (\/) X <> EmptyMS I
proof
  assume that
A1: I is non empty and
A2: {x,y} (\/) X = EmptyMS I;
  consider i being object such that
A3: i in I by A1,XBOOLE_0:def 1;
  {x.i,y.i} \/ X.i <> {};
  then {x,y}.i \/ X.i <> {} by A3,Def2;
  then ({x,y} (\/) X).i <> {} by A3,PBOOLE:def 4;
  hence contradiction by A2,PBOOLE:5;
end;

begin :: Intersection of an unordered pairs (or a singelton) and a set

theorem     :: ZFMISC_1:51
  X (/\) {x} = {x} implies x in X
proof
  assume
A1: X (/\) {x} = {x};
  let i;
  assume
A2: i in I;
  then X.i /\ {x.i} = X.i /\ {x}.i by Def1
    .= (X (/\) {x}).i by A2,PBOOLE:def 5
    .= {x.i} by A1,A2,Def1;
  hence thesis by ZFMISC_1:45;
end;

theorem     :: ZFMISC_1:52
  x in X implies X (/\) {x} = {x}
proof
  assume
A1: x in X;
  now
    let i be object;
    assume
A2: i in I;
    then
A3: x.i in X.i by A1;
    thus (X (/\) {x}).i = X.i /\ {x}.i by A2,PBOOLE:def 5
      .= X.i /\ {x.i} by A2,Def1
      .= {x.i} by A3,ZFMISC_1:46
      .= {x}.i by A2,Def1;
  end;
  hence X (/\) {x} = {x};
end;

theorem     :: ZFMISC_1:53, 63
  x in X & y in X iff {x,y} (/\) X = {x,y}
proof
  thus x in X & y in X implies {x,y} (/\) X = {x,y}
  proof
    assume that
A1: x in X and
A2: y in X;
    now
      let i be object;
      assume
A3:   i in I;
      then
A4:   x.i in X.i by A1;
A5:   y.i in X.i by A2,A3;
      thus ({x,y} (/\) X).i = {x,y}.i /\ X.i by A3,PBOOLE:def 5
        .= {x.i,y.i} /\ X.i by A3,Def2
        .= {x.i,y.i} by A4,A5,ZFMISC_1:47
        .= {x,y}.i by A3,Def2;
    end;
    hence thesis;
  end;
  assume
A6: {x,y} (/\) X = {x,y};
  thus x in X
  proof
    let i;
    assume
A7: i in I;
    then {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2
      .= ({x,y} (/\) X).i by A7,PBOOLE:def 5
      .= {x.i,y.i} by A6,A7,Def2;
    hence thesis by ZFMISC_1:55;
  end;
  let i;
  assume
A8: i in I;
  then {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2
    .= ({x,y} (/\) X).i by A8,PBOOLE:def 5
    .= {x.i,y.i} by A6,A8,Def2;
  hence thesis by ZFMISC_1:55;
end;

theorem     :: ZFMISC_1:54
  I is non empty & {x} (/\) X = EmptyMS I implies not x in X
proof
  assume that
A1: I is non empty and
A2: {x} (/\) X = EmptyMS I and
A3: x in X;
  consider i being object such that
A4: i in I by A1,XBOOLE_0:def 1;
  {x.i} /\ X.i = {x}.i /\ X.i by A4,Def1
    .= ({x} (/\) X).i by A4,PBOOLE:def 5
    .= {} by A2,PBOOLE:5;
  then {x.i} misses X.i by XBOOLE_0:def 7;
  then not x.i in X.i by ZFMISC_1:48;
  hence contradiction by A3,A4;
end;

theorem     :: ZFMISC_1:55
  I is non empty & {x,y} (/\) X = EmptyMS I implies not x in X & not y in X
proof
  assume that
A1: I is non empty and
A2: {x,y} (/\) X = EmptyMS I;
A3: now
    let i;
    assume
A4: i in I;
    hence {x.i,y.i} /\ X.i = {x,y}.i /\ X.i by Def2
      .= ({x,y} (/\) X).i by A4,PBOOLE:def 5
      .= {} by A2,PBOOLE:5;
  end;
  thus not x in X
  proof
    assume
A5: x in X;
    now
      consider i being object such that
A6:   i in I by A1,XBOOLE_0:def 1;
      take i;
      {x.i,y.i} /\ X.i = {} by A3,A6;
      then {x.i,y.i} misses X.i by XBOOLE_0:def 7;
      hence i in I & not x.i in X.i by A6,ZFMISC_1:49;
    end;
    hence contradiction by A5;
  end;
  assume
A7: y in X;
  now
    consider i being object such that
A8: i in I by A1,XBOOLE_0:def 1;
    take i;
    {x.i,y.i} /\ X.i = {} by A3,A8;
    then {x.i,y.i} misses X.i by XBOOLE_0:def 7;
    hence i in I & not y.i in X.i by A8,ZFMISC_1:49;
  end;
  hence contradiction by A7;
end;

begin :: Difference of an unordered pairs (or a singelton) and a set

theorem     :: ZFMISC_1:64 a
  y in X (\) {x} implies y in X
proof
  assume
A1: y in X (\) {x};
  let i;
  assume
A2: i in I;
  then y.i in (X (\) {x}).i by A1;
  then y.i in X.i \ {x}.i by A2,PBOOLE:def 6;
  then y.i in X.i \ {x.i} by A2,Def1;
  hence thesis by ZFMISC_1:56;
end;

theorem     :: ZFMISC_1:64 b
  I is non empty & y in X (\) {x} implies y <> x
proof
  assume that
A1: I is non empty and
A2: y in X (\) {x};
  consider i being object such that
A3: i in I by A1,XBOOLE_0:def 1;
  now
    take i;
    y.i in (X (\) {x}).i by A2,A3;
    then y.i in X.i \ {x}.i by A3,PBOOLE:def 6;
    then y.i in X.i \ {x.i} by A3,Def1;
    hence y.i <> x.i by ZFMISC_1:56;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:65
  I is non empty & X (\) {x} = X implies not x in X
proof
  assume that
A1: I is non empty and
A2: X (\) {x} = X and
A3: x in X;
A4: now
    let i;
    assume
A5: i in I;
    hence X.i \ {x.i} = X.i \ {x}.i by Def1
      .= X.i by A2,A5,PBOOLE:def 6;
  end;
  now
    consider i being object such that
A6: i in I by A1,XBOOLE_0:def 1;
    take i;
    thus i in I by A6;
    X.i \ {x.i} = X.i by A4,A6;
    hence not x.i in X.i by ZFMISC_1:57;
  end;
  hence contradiction by A3;
end;

theorem     :: ZFMISC_1:67
  I is non empty & {x} (\) X = {x} implies not x in X
proof
  assume that
A1: I is non empty and
A2: {x} (\) X = {x} and
A3: x in X;
  consider i being object such that
A4: i in I by A1,XBOOLE_0:def 1;
  {x.i} \ X.i = {x}.i \ X.i by A4,Def1
    .= ({x} (\) X).i by A4,PBOOLE:def 6
    .= {x.i} by A2,A4,Def1;
  then not x.i in X.i by ZFMISC_1:59;
  hence contradiction by A3,A4;
end;

theorem     :: ZFMISC_1:68
  {x} (\) X = EmptyMS I iff x in X
proof
  thus {x} (\) X = EmptyMS I implies x in X
  proof
    assume
A1: {x} (\) X = EmptyMS I;
    let i;
    assume
A2: i in I;
    then {x.i} \ X.i = {x}.i \ X.i by Def1
      .= ({x} (\) X).i by A2,PBOOLE:def 6
      .= {} by A1,PBOOLE:5;
    hence thesis by ZFMISC_1:60;
  end;
  assume
A3: x in X;
  now
    let i be object;
    assume
A4: i in I;
    then
A5: x.i in X.i by A3;
    thus ({x} (\) X).i = {x}.i \ X.i by A4,PBOOLE:def 6
      .= {x.i} \ X.i by A4,Def1
      .= {} by A5,ZFMISC_1:60
      .= EmptyMS I.i by PBOOLE:5;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:70
  I is non empty & {x,y} (\) X = {x} implies not x in X
proof
  assume that
A1: I is non empty and
A2: {x,y} (\) X = {x};
  consider i being object such that
A3: i in I by A1,XBOOLE_0:def 1;
  {x.i,y.i} \ X.i = {x,y}.i \ X.i by A3,Def2
    .= ({x,y} (\) X).i by A3,PBOOLE:def 6
    .= {x.i} by A2,A3,Def1;
  then not x.i in X.i by ZFMISC_1:62;
  hence thesis by A3;
end;

theorem     :: ZFMISC_1:72
  I is non empty & {x,y} (\) X = {x,y} implies not x in X & not y in X
proof
  assume I is non empty;
  then consider i being object such that
A1: i in I by XBOOLE_0:def 1;
    assume
A2: {x,y} (\) X = {x,y};
    thus not x in X
    proof
      assume
A3:   x in X;
      {x.i,y.i} \ X.i = {x,y}.i \ X.i by A1,Def2
        .= ({x,y} (\) X).i by A1,PBOOLE:def 6
        .= {x.i,y.i} by A1,A2,Def2;
      then not x.i in X.i by ZFMISC_1:63;
      hence contradiction by A1,A3;
    end;
    assume
A4: y in X;
    {x.i,y.i} \ X.i = {x,y}.i \ X.i by A1,Def2
      .= ({x,y} (\) X).i by A1,PBOOLE:def 6
      .= {x.i,y.i} by A1,A2,Def2;
    then not y.i in X.i by ZFMISC_1:63;
    hence contradiction by A1,A4;
end;

theorem     :: ZFMISC_1:73
  {x,y} (\) X = EmptyMS I iff x in X & y in X
proof
  thus {x,y} (\) X = EmptyMS I implies x in X & y in X
  proof
    assume
A1: {x,y} (\) X = EmptyMS I;
    thus x in X
    proof
      let i;
      assume
A2:   i in I;
      then {x.i,y.i} \ X.i = {x,y}.i \ X.i by Def2
        .= ({x,y} (\) X).i by A2,PBOOLE:def 6
        .= {} by A1,PBOOLE:5;
      hence thesis by ZFMISC_1:64;
    end;
    let i;
    assume
A3: i in I;
    then {x.i,y.i} \ X.i = {x,y}.i \ X.i by Def2
      .= ({x,y} (\) X).i by A3,PBOOLE:def 6
      .= {} by A1,PBOOLE:5;
    hence thesis by ZFMISC_1:64;
  end;
  assume that
A4: x in X and
A5: y in X;
  now
    let i be object;
    assume
A6: i in I;
    then
A7: x.i in X.i by A4;
A8: y.i in X.i by A5,A6;
    thus ({x,y} (\) X).i = {x,y}.i \ X.i by A6,PBOOLE:def 6
      .= {x.i,y.i} \ X.i by A6,Def2
      .= {} by A7,A8,ZFMISC_1:64
      .= EmptyMS I.i by PBOOLE:5;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:75
  X = EmptyMS I or X = {x} or X = {y} or X = {x,y}
    implies X (\) {x,y} = EmptyMS I
proof
  assume
A1: X = EmptyMS I or X = {x} or X = {y} or X = {x,y};
  now
    let i be object such that
A2: i in I;
    per cases by A1;
    suppose X = EmptyMS I;
      then
A3:   X.i = {} by PBOOLE:5;
      thus (X (\) {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 6
        .= EmptyMS I.i by A3,PBOOLE:5;
    end;
    suppose X = {x};
      then
A4:   X.i = {x.i} by A2,Def1;
      thus (X (\) {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 6
        .= X.i \ {x.i,y.i} by A2,Def2
        .= {} by A4,ZFMISC_1:66
        .= EmptyMS I.i by PBOOLE:5;
    end;
    suppose X = {y};
      then
A5:   X.i = {y.i} by A2,Def1;
      thus (X (\) {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 6
        .= X.i \ {x.i,y.i} by A2,Def2
        .= {} by A5,ZFMISC_1:66
        .= EmptyMS I.i by PBOOLE:5;
    end;
    suppose X = {x,y};
      then
A6:   X.i = {x.i,y.i} by A2,Def2;
      thus (X (\) {x,y}).i = X.i \ {x,y}.i by A2,PBOOLE:def 6
        .= X.i \ {x.i,y.i} by A2,Def2
        .= {} by A6,ZFMISC_1:66
        .= EmptyMS I.i by PBOOLE:5;
    end;
  end;
  hence thesis;
end;

begin :: Cartesian product

theorem     :: ZFMISC_1:113
  X = EmptyMS I or Y = EmptyMS I implies [|X,Y|] = EmptyMS I
proof
  assume
A1: X = EmptyMS I or Y = EmptyMS I;
  per cases by A1;
  suppose
A2: X = EmptyMS I;
    now
      let i be object;
      assume
A3:   i in I;
A4:   X.i = {} by A2,PBOOLE:5;
      thus [|X,Y|].i = [:X.i,Y.i:] by A3,PBOOLE:def 16
        .= {} by A4,ZFMISC_1:90
        .= EmptyMS I.i by PBOOLE:5;
    end;
    hence thesis;
  end;
  suppose
A5: Y = EmptyMS I;
    now
      let i be object;
      assume
A6:   i in I;
A7:   Y.i = {} by A5,PBOOLE:5;
      thus [|X,Y|].i = [:X.i,Y.i:] by A6,PBOOLE:def 16
        .= {} by A7,ZFMISC_1:90
        .= EmptyMS I.i by PBOOLE:5;
    end;
    hence thesis;
  end;
end;

theorem     :: ZFMISC_1:114
  X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y
proof
  assume that
A1: X is non-empty and
A2: Y is non-empty and
A3: [|X,Y|] = [|Y,X|];
  now
    let i be object;
    assume
A4: i in I;
    then
A5: X.i is non empty by A1;
A6: Y.i is non empty by A2,A4;
    [:X.i,Y.i:] = [|X,Y|].i by A4,PBOOLE:def 16
      .= [:Y.i,X.i:] by A3,A4,PBOOLE:def 16;
    hence X.i = Y.i by A5,A6,ZFMISC_1:91;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:115
  [|X,X|] = [|Y,Y|] implies X = Y
proof
  assume
A1: [|X,X|] = [|Y,Y|];
  now
    let i be object;
    assume
A2: i in I;
    then [:X.i,X.i:] = [|X,X|].i by PBOOLE:def 16
      .= [:Y.i,Y.i:] by A1,A2,PBOOLE:def 16;
    hence X.i = Y.i by ZFMISC_1:92;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:117
  Z is non-empty & ([|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]) implies X c= Y
proof
  assume that
A1: Z is non-empty and
A2: [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|];
  per cases by A2;
  suppose
A3: [|X,Z|] c= [|Y,Z|];
    let i;
    assume
A4: i in I;
    then
A5: Z.i is non empty by A1;
    [|X,Z|].i c= [|Y,Z|].i by A3,A4;
    then [:X.i,Z.i:] c= [|Y,Z|].i by A4,PBOOLE:def 16;
    then [:X.i,Z.i:] c= [:Y.i,Z.i:] by A4,PBOOLE:def 16;
    hence thesis by A5,ZFMISC_1:94;
  end;
  suppose
A6: [|Z,X|] c= [|Z,Y|];
    let i;
    assume
A7: i in I;
    then
A8: Z.i is non empty by A1;
    [|Z,X|].i c= [|Z,Y|].i by A6,A7;
    then [:Z.i,X.i:] c= [|Z,Y|].i by A7,PBOOLE:def 16;
    then [:Z.i,X.i:] c= [:Z.i,Y.i:] by A7,PBOOLE:def 16;
    hence thesis by A8,ZFMISC_1:94;
  end;
end;

theorem     :: ZFMISC_1:118
  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 i;
    assume
A2: i in I;
    then X.i c= Y.i by A1;
    then [:X.i,Z.i:] c= [:Y.i,Z.i:] by ZFMISC_1:95;
    then [|X,Z|].i c= [:Y.i,Z.i:] by A2,PBOOLE:def 16;
    hence thesis by A2,PBOOLE:def 16;
  end;
  let i;
  assume
A3: i in I;
  then X.i c= Y.i by A1;
  then [:Z.i,X.i:] c= [:Z.i,Y.i:] by ZFMISC_1:95;
  then [|Z,X|].i c= [:Z.i,Y.i:] by A3,PBOOLE:def 16;
  hence thesis by A3,PBOOLE:def 16;
end;

theorem     :: ZFMISC_1:119
  x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|]
proof
  assume that
A1: x1 c= A and
A2: x2 c= B;
  let i;
  assume
A3: i in I;
  then
A4: x1.i c= A.i by A1;
  x2.i c= B.i by A2,A3;
  then [:x1.i,x2.i:] c= [:A.i,B.i:] by A4,ZFMISC_1:96;
  then [|x1,x2|].i c= [:A.i,B.i:] by A3,PBOOLE:def 16;
  hence thesis by A3,PBOOLE:def 16;
end;

theorem     :: ZFMISC_1:120
  [|X (\/) Y, Z|] = [|X, Z|] (\/) [|Y, Z|] &
  [|Z, X (\/) Y|] = [|Z, X|] (\/) [|Z, Y|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence [|X (\/) Y, Z|].i = [:(X (\/) Y).i, Z.i:] by PBOOLE:def 16
      .= [:X.i \/ Y.i, Z.i:] by A1,PBOOLE:def 4
      .= [:X.i, Z.i:] \/ [:Y.i, Z.i:] by ZFMISC_1:97
      .= [|X,Z|].i \/ [:Y.i, Z.i:] by A1,PBOOLE:def 16
      .= [|X,Z|].i \/ [|Y,Z|].i by A1,PBOOLE:def 16
      .= ([|X, Z|] (\/) [|Y, Z|]).i by A1,PBOOLE:def 4;
  end;
  hence [|X (\/) Y, Z|] = [|X, Z|] (\/) [|Y, Z|];
  now
    let i be object;
    assume
A2: i in I;
    hence [|Z, X (\/) Y|].i = [:Z.i, (X (\/) Y).i:] by PBOOLE:def 16
      .= [:Z.i, X.i \/ Y.i:] by A2,PBOOLE:def 4
      .= [:Z.i,X.i:] \/ [:Z.i,Y.i:] by ZFMISC_1:97
      .= [|Z,X|].i \/ [:Z.i,Y.i:] by A2,PBOOLE:def 16
      .= [|Z,X|].i \/ [|Z,Y|].i by A2,PBOOLE:def 16
      .= ([|Z,X|] (\/) [|Z,Y|]).i by A2,PBOOLE:def 4;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:121
  [|x1 (\/) x2, A (\/) B|] = [|x1,A|] (\/) [|x1,B|] (\/) [|x2,A|] (\/) [|x2,B|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence [|x1 (\/) x2, A (\/) B|].i = [:(x1 (\/) x2).i,(A (\/) B).i:]
                      by PBOOLE:def 16
      .= [:x1.i \/ x2.i, (A (\/) B).i:] by A1,PBOOLE:def 4
      .= [:x1.i \/ x2.i, A.i \/ B.i:] by A1,PBOOLE:def 4
      .= [:x1.i,A.i:] \/ [:x1.i,B.i:] \/ [:x2.i,A.i:] \/ [:x2.i,B.i:]
    by ZFMISC_1:98
      .= [|x1,A|].i \/ [:x1.i,B.i:] \/ [:x2.i,A.i:] \/ [:x2.i,B.i:]
    by A1,PBOOLE:def 16
      .= [|x1,A|].i \/ [|x1,B|].i \/ [:x2.i,A.i:] \/ [:x2.i,B.i:]
    by A1,PBOOLE:def 16
      .= [|x1,A|].i \/ [|x1,B|].i \/ [|x2,A|].i \/ [:x2.i,B.i:]
    by A1,PBOOLE:def 16
      .= [|x1,A|].i \/ [|x1,B|].i \/ [|x2,A|].i \/ [|x2,B|].i
    by A1,PBOOLE:def 16
      .= ([|x1,A|] (\/) [|x1,B|]).i \/ [|x2,A|].i \/ [|x2,B|].i
    by A1,PBOOLE:def 4
      .= ([|x1,A|] (\/) [|x1,B|] (\/) [|x2,A|]).i \/ [|x2,B|].i
    by A1,PBOOLE:def 4
      .= ([|x1,A|] (\/) [|x1,B|] (\/) [|x2,A|] (\/) [|x2,B|]).i
           by A1,PBOOLE:def 4;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:122
  [|X (/\) Y, Z|] = [|X, Z|] (/\) [|Y, Z|] &
   [|Z, X (/\) Y|] = [|Z, X|] (/\) [|Z, Y|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence [|X (/\) Y, Z|].i = [:(X (/\) Y).i,Z.i:] by PBOOLE:def 16
      .= [:X.i /\ Y.i,Z.i:] by A1,PBOOLE:def 5
      .= [:X.i,Z.i:] /\ [:Y.i,Z.i:] by ZFMISC_1:99
      .= [|X,Z|].i /\ [:Y.i,Z.i:] by A1,PBOOLE:def 16
      .= [|X,Z|].i /\ [|Y,Z|].i by A1,PBOOLE:def 16
      .= ([|X, Z|] (/\) [|Y, Z|]).i by A1,PBOOLE:def 5;
  end;
  hence [|X (/\) Y, Z|] = [|X, Z|] (/\) [|Y, Z|];
  now
    let i be object;
    assume
A2: i in I;
    hence [|Z,X (/\) Y|].i = [:Z.i,(X (/\) Y).i:] by PBOOLE:def 16
      .= [:Z.i,X.i /\ Y.i:] by A2,PBOOLE:def 5
      .= [:Z.i,X.i:] /\ [:Z.i,Y.i:] by ZFMISC_1:99
      .= [|Z,X|].i /\ [:Z.i,Y.i:] by A2,PBOOLE:def 16
      .= [|Z,X|].i /\ [|Z,Y|].i by A2,PBOOLE:def 16
      .= ([|Z,X|] (/\) [|Z,Y|]).i by A2,PBOOLE:def 5;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:123
  [|x1 (/\) x2, A (/\) B|] = [|x1,A|] (/\) [|x2, B|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence [|x1 (/\) x2, A (/\) B|].i
       = [:(x1 (/\) x2).i,(A (/\) B).i:] by PBOOLE:def 16
      .= [:x1.i /\ x2.i,(A (/\) B).i:] by A1,PBOOLE:def 5
      .= [:x1.i /\ x2.i,A.i /\ B.i:] by A1,PBOOLE:def 5
      .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by ZFMISC_1:100
      .= [|x1,A|].i /\ [:x2.i,B.i:] by A1,PBOOLE:def 16
      .= [|x1,A|].i /\ [|x2,B|].i by A1,PBOOLE:def 16
      .= ([|x1,A|] (/\) [|x2, B|]).i by A1,PBOOLE:def 5;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:124
  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;
  now
    let i be object;
    assume
A3: i in I;
    then
A4: A.i c= X.i by A1;
A5: B.i c= Y.i by A2,A3;
    thus ([|A,Y|] (/\) [|X,B|]).i
       = [|A,Y|].i /\ [|X,B|].i by A3,PBOOLE:def 5
      .= [:A.i,Y.i:] /\ [|X,B|].i by A3,PBOOLE:def 16
      .= [:A.i,Y.i:] /\ [:X.i,B.i:] by A3,PBOOLE:def 16
      .= [:A.i,B.i:] by A4,A5,ZFMISC_1:101
      .= [|A,B|].i by A3,PBOOLE:def 16;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:125
  [|X (\) Y, Z|] = [|X, Z|] (\) [|Y, Z|] &
  [|Z, X (\) Y|] = [|Z, X|] (\) [|Z, Y|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence [|X (\) Y, Z|].i = [:(X (\) Y).i,Z.i:] by PBOOLE:def 16
      .= [:X.i \ Y.i,Z.i:] by A1,PBOOLE:def 6
      .= [:X.i,Z.i:] \ [:Y.i,Z.i:] by ZFMISC_1:102
      .= [|X,Z|].i \ [:Y.i,Z.i:] by A1,PBOOLE:def 16
      .= [|X,Z|].i \ [|Y,Z|].i by A1,PBOOLE:def 16
      .= ([|X, Z|] (\) [|Y, Z|]).i by A1,PBOOLE:def 6;
  end;
  hence [|X (\) Y, Z|] = [|X, Z|] (\) [|Y, Z|];
  now
    let i be object;
    assume
A2: i in I;
    hence [|Z,X (\) Y|].i = [:Z.i,(X (\) Y).i:] by PBOOLE:def 16
      .= [:Z.i,X.i \ Y.i:] by A2,PBOOLE:def 6
      .= [:Z.i,X.i:] \ [:Z.i,Y.i:] by ZFMISC_1:102
      .= [|Z,X|].i \ [:Z.i,Y.i:] by A2,PBOOLE:def 16
      .= [|Z,X|].i \ [|Z,Y|].i by A2,PBOOLE:def 16
      .= ([|Z,X|] (\) [|Z,Y|]).i by A2,PBOOLE:def 6;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:126
  [|x1,x2|] (\) [|A,B|] = [|x1(\)A,x2|] (\/) [|x1,x2(\)B|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence ([|x1,x2|] (\) [|A,B|]).i = [|x1,x2|].i \ [|A,B|].i by PBOOLE:def 6
      .= [:x1.i,x2.i:] \ [|A,B|].i by A1,PBOOLE:def 16
      .= [:x1.i,x2.i:] \ [:A.i,B.i:] by A1,PBOOLE:def 16
      .= [:x1.i\A.i,x2.i:] \/ [:x1.i,x2.i\B.i:] by ZFMISC_1:103
      .= [:(x1(\)A).i,x2.i:] \/ [:x1.i,x2.i\B.i:] by A1,PBOOLE:def 6
      .= [:(x1(\)A).i,x2.i:] \/ [:x1.i,(x2(\)B).i:] by A1,PBOOLE:def 6
      .= [|x1(\)A,x2|].i \/ [:x1.i,(x2(\)B).i:] by A1,PBOOLE:def 16
      .= [|x1(\)A,x2|].i \/ [|x1,x2(\)B|].i by A1,PBOOLE:def 16
      .= ([|x1(\)A,x2|] (\/) [|x1,x2(\)B|]).i by A1,PBOOLE:def 4;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:127
  x1 (/\) x2 = EmptyMS I or A (/\) B = EmptyMS I
  implies [|x1,A|] (/\) [|x2,B|] = EmptyMS I
proof
  assume
A1: x1 (/\) x2 = EmptyMS I or A (/\) B= EmptyMS I;
  per cases by A1;
  suppose
A2: x1 (/\) x2 = EmptyMS I;
    now
      let i be object;
      assume
A3:   i in I;
      then x1.i /\ x2.i = (x1 (/\) x2).i by PBOOLE:def 5
        .= {} by A2,PBOOLE:5;
      then x1.i misses x2.i by XBOOLE_0:def 7;
      then
A4:   [:x1.i,A.i:] misses [:x2.i,B.i:] by ZFMISC_1:104;
      thus ([|x1,A|] (/\) [|x2,B|]).i = [|x1,A|].i /\ [|x2,B|].i
      by A3,PBOOLE:def 5
        .= [:x1.i,A.i:] /\ [|x2,B|].i by A3,PBOOLE:def 16
        .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by A3,PBOOLE:def 16
        .= {} by A4,XBOOLE_0:def 7
        .= EmptyMS I.i by PBOOLE:5;
    end;
    hence thesis;
  end;
  suppose
A5: A (/\) B = EmptyMS I;
    now
      let i be object;
      assume
A6:   i in I;
      then A.i /\ B.i = (A (/\) B).i by PBOOLE:def 5
        .= {} by A5,PBOOLE:5;
      then A.i misses B.i by XBOOLE_0:def 7;
      then
A7:   [:x1.i,A.i:] misses [:x2.i,B.i:] by ZFMISC_1:104;
      thus ([|x1,A|] (/\) [|x2,B|]).i = [|x1,A|].i /\ [|x2,B|].i
      by A6,PBOOLE:def 5
        .= [:x1.i,A.i:] /\ [|x2,B|].i by A6,PBOOLE:def 16
        .= [:x1.i,A.i:] /\ [:x2.i,B.i:] by A6,PBOOLE:def 16
        .= {} by A7,XBOOLE_0:def 7
        .= EmptyMS I.i by PBOOLE:5;
    end;
    hence thesis;
  end;
end;

theorem     :: ZFMISC_1:130
  X is non-empty implies [|{x},X|] is non-empty & [|X,{x}|] is non-empty
proof
  assume
A1: X is non-empty;
  thus [|{x},X|] is non-empty
  proof
    let i be object;
    assume
A2: i in I;
    then X.i is non empty by A1;
    then [:{x.i},X.i:] is non empty by ZFMISC_1:107;
    then [:{x}.i,X.i:] is non empty by A2,Def1;
    hence thesis by A2,PBOOLE:def 16;
  end;
  let i be object;
  assume
A3: i in I;
  then X.i is non empty by A1;
  then [:X.i,{x.i}:] is non empty by ZFMISC_1:107;
  then [:X.i,{x}.i:] is non empty by A3,Def1;
  hence thesis by A3,PBOOLE:def 16;
end;

theorem     :: ZFMISC_1:132
  [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] &
  [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|]
proof
  now
    let i be object;
    assume
A1: i in I;
    hence [|{x,y},X|].i = [:{x,y}.i,X.i:] by PBOOLE:def 16
      .= [:{x.i,y.i},X.i:] by A1,Def2
      .= [:{x.i},X.i:] \/ [:{y.i},X.i:] by ZFMISC_1:109
      .= [:{x}.i,X.i:] \/ [:{y.i},X.i:] by A1,Def1
      .= [:{x}.i,X.i:] \/ [:{y}.i,X.i:] by A1,Def1
      .= [|{x},X|].i \/ [:{y}.i,X.i:] by A1,PBOOLE:def 16
      .= [|{x},X|].i \/ [|{y},X|].i by A1,PBOOLE:def 16
      .= ([|{x},X|] (\/) [|{y},X|]).i by A1,PBOOLE:def 4;
  end;
  hence [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|];
  now
    let i be object;
    assume
A2: i in I;
    hence [|X,{x,y}|].i = [:X.i,{x,y}.i:] by PBOOLE:def 16
      .= [:X.i,{x.i,y.i}:] by A2,Def2
      .= [:X.i,{x.i}:] \/ [:X.i,{y.i}:] by ZFMISC_1:109
      .= [:X.i,{x}.i:] \/ [:X.i,{y.i}:] by A2,Def1
      .= [:X.i,{x}.i:] \/ [:X.i,{y}.i:] by A2,Def1
      .= [|X,{x}|].i \/ [:X.i,{y}.i:] by A2,PBOOLE:def 16
      .= [|X,{x}|].i \/ [|X,{y}|].i by A2,PBOOLE:def 16
      .= ([|X,{x}|] (\/) [|X,{y}|]).i by A2,PBOOLE:def 4;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:134
  x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|]
  implies x1 = x2 & A = B
proof
  assume that
A1: x1 is non-empty and
A2: A is non-empty and
A3: [|x1,A|] = [|x2,B|];
  now
    let i be object;
    assume
A4: i in I;
    then
A5: x1.i is non empty by A1;
A6: A.i is non empty by A2,A4;
    [:x1.i,A.i:] = [|x1,A|].i by A4,PBOOLE:def 16
      .= [:x2.i,B.i:] by A3,A4,PBOOLE:def 16;
    hence x1.i = x2.i by A5,A6,ZFMISC_1:110;
  end;
  hence x1 = x2;
  now
    let i be object;
    assume
A7: i in I;
    then
A8: x1.i is non empty by A1;
A9: A.i is non empty by A2,A7;
    [:x1.i,A.i:] = [|x1,A|].i by A7,PBOOLE:def 16
      .= [:x2.i,B.i:] by A3,A7,PBOOLE:def 16;
    hence A.i = B.i by A8,A9,ZFMISC_1:110;
  end;
  hence thesis;
end;

theorem     :: ZFMISC_1:116, 135
  X c= [|X,Y|] or X c= [|Y,X|] implies X = EmptyMS I
proof
  assume
A1: X c= [|X,Y|] or X c= [|Y,X|];
  per cases by A1;
  suppose
A2: X c= [|X,Y|];
    now
      let i be object;
      assume
A3:   i in I;
      then X.i c= [|X,Y|].i by A2;
      then X.i c= [:X.i,Y.i:] by A3,PBOOLE:def 16;
      hence X.i = {} by ZFMISC_1:111
        .= EmptyMS I.i by PBOOLE:5;
    end;
    hence thesis;
  end;
  suppose
A4: X c= [|Y,X|];
    now
      let i be object;
      assume
A5:   i in I;
      then X.i c= [|Y,X|].i by A4;
      then X.i c= [:Y.i,X.i:] by A5,PBOOLE:def 16;
      hence X.i = {} by ZFMISC_1:111
        .= EmptyMS I.i by PBOOLE:5;
    end;
    hence thesis;
  end;
end;

theorem     :: BORSUK_1:2
  A in [|x,y|] & A in [|X,Y|] implies A in [|x (/\) X, y (/\) Y|]
proof
  assume that
A1: A in [|x,y|] and
A2: A in [|X,Y|];
  let i;
  assume
A3: i in I;
  then
A4: A.i in [|x,y|].i by A1;
A5: A.i in [|X,Y|].i by A2,A3;
A6: A.i in [:x.i,y.i:] by A3,A4,PBOOLE:def 16;
  A.i in [:X.i,Y.i:] by A3,A5,PBOOLE:def 16;
  then A.i in [:x.i /\ X.i, y.i /\ Y.i:] by A6,ZFMISC_1:113;
  then A.i in [:(x (/\) X).i, y.i /\ Y.i:] by A3,PBOOLE:def 5;
  then A.i in [:(x (/\) X).i, (y (/\) Y).i:] by A3,PBOOLE:def 5;
  hence thesis by A3,PBOOLE:def 16;
end;

theorem     :: BORSUK_1:7
  [|x,X|] c= [|y,Y|] & [|x,X|] is non-empty implies x c= y & X c= Y
proof
  assume that
A1: [|x,X|] c= [|y,Y|] and
A2: [|x,X|] is non-empty;
  thus x c= y
  proof
    let i;
    assume
A3: i in I;
    then [|x,X|].i c= [|y,Y|].i by A1;
    then [:x.i,X.i:] c= [|y,Y|].i by A3,PBOOLE:def 16;
    then
A4: [:x.i,X.i:] c= [:y.i,Y.i:] by A3,PBOOLE:def 16;
    [|x,X|].i is non empty by A2,A3;
    then [:x.i,X.i:] is non empty by A3,PBOOLE:def 16;
    hence thesis by A4,ZFMISC_1:114;
  end;
  let i;
  assume
A5: i in I;
  then [|x,X|].i c= [|y,Y|].i by A1;
  then [:x.i,X.i:] c= [|y,Y|].i by A5,PBOOLE:def 16;
  then
A6: [:x.i,X.i:] c= [:y.i,Y.i:] by A5,PBOOLE:def 16;
  [|x,X|].i is non empty by A2,A5;
  then [:x.i,X.i:] is non empty by A5,PBOOLE:def 16;
  hence thesis by A6,ZFMISC_1:114;
end;

theorem     :: REALSET1:4
  A c= X implies [|A,A|] c= [|X,X|]
proof
  assume
A1: A c= X;
  let i;
  assume
A2: i in I;
  then A.i c= X.i by A1;
  then [:A.i,A.i:] c= [:X.i,X.i:] by ZFMISC_1:96;
  then [|A,A|].i c= [:X.i,X.i:] by A2,PBOOLE:def 16;
  hence thesis by A2,PBOOLE:def 16;
end;

theorem     :: SYSREL:17
  X (/\) Y = EmptyMS I implies [|X,Y|] (/\) [|Y,X|] = EmptyMS I
proof
  assume
A1: X (/\) Y = EmptyMS I;
  now
    let i be object;
    assume
A2: i in I;
    then X.i /\ Y.i = (X (/\) Y).i by PBOOLE:def 5
      .= {} by A1,PBOOLE:5;
    then X.i misses Y.i by XBOOLE_0:def 7;
    then
A3: [:X.i,Y.i:] misses [:Y.i,X.i:] by ZFMISC_1:104;
    thus ([|X,Y|] (/\) [|Y,X|]).i = [|X,Y|].i /\ [|Y,X|].i by A2,PBOOLE:def 5
      .= [:X.i,Y.i:] /\ [|Y,X|].i by A2,PBOOLE:def 16
      .= [:X.i,Y.i:] /\ [:Y.i,X.i:] by A2,PBOOLE:def 16
      .= {} by A3,XBOOLE_0:def 7
      .= EmptyMS I.i by PBOOLE:5;
  end;
  hence thesis;
end;

theorem     :: ALTCAT_1:1
  A is non-empty & ([|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]) implies B c= Y
proof
  assume that
A1: A is non-empty and
A2: [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|];
  per cases by A2;
  suppose
A3: [|A,B|] c= [|X,Y|];
    let i;
    assume
A4: i in I;
    then [|A,B|].i c= [|X,Y|].i by A3;
    then [:A.i,B.i:] c= [|X,Y|].i by A4,PBOOLE:def 16;
    then
A5: [:A.i,B.i:] c= [:X.i,Y.i:] by A4,PBOOLE:def 16;
    A.i is non empty by A1,A4;
    hence thesis by A5,ZFMISC_1:115;
  end;
  suppose
A6: [|B,A|] c= [|Y,X|];
    let i;
    assume
A7: i in I;
    then [|B,A|].i c= [|Y,X|].i by A6;
    then [:B.i,A.i:] c= [|Y,X|].i by A7,PBOOLE:def 16;
    then
A8: [:B.i,A.i:] c= [:Y.i,X.i:] by A7,PBOOLE:def 16;
    A.i is non empty by A1,A7;
    hence thesis by A8,ZFMISC_1:115;
  end;
end;

theorem     :: PARTFUN1:1
  x c= [|A,B|] & y c= [|X,Y|] implies x (\/) y c= [|A (\/) X,B (\/) Y|]
proof
  assume that
A1: x c= [|A,B|] and
A2: y c= [|X,Y|];
  let i;
  assume
A3: i in I;
  then
A4: x.i c= [|A,B|].i by A1;
A5: y.i c= [|X,Y|].i by A2,A3;
A6: x.i c= [:A.i,B.i:] by A3,A4,PBOOLE:def 16;
  y.i c= [:X.i,Y.i:] by A3,A5,PBOOLE:def 16;
  then x.i \/ y.i c= [:A.i \/ X.i,B.i \/ Y.i:] by A6,ZFMISC_1:119;
  then (x (\/) y).i c= [:A.i \/ X.i,B.i \/ Y.i:] by A3,PBOOLE:def 4;
  then (x (\/) y).i c= [:(A (\/) X).i,B.i \/ Y.i:] by A3,PBOOLE:def 4;
  then (x (\/) y).i c= [:(A (\/) X).i,(B (\/) Y).i:] by A3,PBOOLE:def 4;
  hence thesis by A3,PBOOLE:def 16;
end;

begin :: Addenda
:: from AUTALG_1

definition
  let I, A, B;
  pred A is_transformable_to B means
  for i be set st i in I holds B.i = {} implies A.i = {};
  reflexivity;
end;