XTUPLE_0

:: Kuratowski Pairs. {T}uples and Projections
::  by Grzegorz Bancerek, Artur Korni\l owicz and Andrzej Trybulec
::
:: Received December 9, 2011
:: Copyright (c) 2011-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 MCART_1, RECDEF_2, XTUPLE_0, FACIRC_1, RELAT_1, TARSKI, XBOOLE_0;
 notations TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 registrations XBOOLE_0;
 requirements BOOLE;
 definitions TARSKI, XBOOLE_0;
 equalities TARSKI, XBOOLE_0;
 expansions TARSKI, XBOOLE_0;
 theorems ENUMSET1, TARSKI, XBOOLE_0, XBOOLE_1;
 schemes XBOOLE_0;

begin :: Pairs

reserve x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2,z2,z4 for object;

definition let x be object;
 attr x is pair means
:Def1: ex x1,x2 st x = [x1,x2];
end;

registration let x1,x2 be object;
 cluster [x1,x2] -> pair;
 coherence;
end;

Lm1: {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;

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

Lm3: { 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 Th1:
  [x1,x2] = [y1,y2] implies x1 = y1 & x2 = y2
proof
  assume
A1: [x1,x2] = [y1,y2];
  per cases;
  suppose
A2: y1 <> y2;
    then
A3: {x1} <> {y1,y2} by Lm2;
    then {x1} = {y1} by A1,Lm3;
   then x1 in {y1} by TARSKI:def 1;
   hence
A4: x1 = y1 by TARSKI:def 1;
    {y1,y2} = {x1,x2} by A1,A3,Lm3;
   hence thesis by A2,A4,Lm3;
  end;
  suppose
A5: y1 = y2;
    then {{x1,x2},{x1}} = {{y1},{y1}} by A1,ENUMSET1:29
        .= {{y1}} by ENUMSET1:29;
    then { y1 } = { x1,x2 } by Lm1;
   hence thesis by A5,Lm1;
  end;
end;

definition
  let x be object;
  assume x is pair;
   then consider x1,x2 such that
A1: x = [x1,x2];
  func x`1 -> object means
:Def2: x = [y1,y2] implies it = y1;
  existence
  proof
    take x1;
    thus thesis by A1,Th1;
  end;
  uniqueness
  proof
    let z1,z2 be object;
    assume that
A2: x = [y1,y2] implies z1 = y1 and
A3: x = [y1,y2] implies z2 = y1;
   thus z1 = x1 by A1,A2
     .= z2 by A1,A3;
  end;
  func x`2 -> object means
:Def3: x = [y1,y2] implies it = y2;
  existence
  proof
    take x2;
    thus thesis by A1,Th1;
  end;
  uniqueness
  proof
    let z1,z2 be object;
    assume that
A4:  x = [y1,y2] implies z1 = y2 and
A5:  x = [y1,y2] implies z2 = y2;
   thus z1 = x2 by A1,A4
    .= z2 by A1,A5;
  end;
end;

registration let x1,x2;
 reduce [x1,x2]`1 to x1;
 reducibility by Def2;
 reduce [x1,x2]`2 to x2;
 reducibility by Def3;
end;

registration
 cluster pair for object;
 existence
 proof
  take [the object, the object], the object, the object;
  thus thesis;
 end;
end;

registration let x be pair object;
 reduce [x`1,x`2] to x;
 reducibility
  proof
   ex x1,x2 st x = [x1,x2] by Def1;
   hence [x`1,x`2] = x;
  end;
end;

theorem
 for a,b being pair object st a`1 = b`1 & a`2 = b`2
  holds a = b
proof let a,b be pair object such that
A1: a`1 = b`1 & a`2 = b`2;
  a = [a`1,a`2] & b = [b`1,b`2];
 hence a = b by A1;
end;

begin :: Triples

definition
  let x1,x2,x3 be object;
  func [x1,x2,x3] -> object equals
  [[x1,x2],x3];
  coherence;
end;

definition let x;
 attr x is triple means
:Def5: ex x1,x2,x3 st x = [x1,x2,x3];
end;

registration let x1,x2,x3;
 cluster [x1,x2,x3] -> triple;
 coherence;
end;

theorem Th3:
  [x1,x2,x3] = [y1,y2,y3] implies x1 = y1 & x2 = y2 & x3 = y3
proof
  assume
A1: [x1,x2,x3] = [y1,y2,y3];
  then [x1,x2] = [y1,y2] by Th1;
  hence thesis by A1,Th1;
end;

registration
 cluster triple for object;
 existence
 proof
  take [the set, the set, the set], the set, the set, the set;
  thus thesis;
 end;
 cluster triple -> pair for object;
 coherence;
end;

definition
  let x be object;
  func x`1_3 -> object equals x`1`1;
   coherence;
  func x`2_3 -> object equals x`1`2;
   coherence;
end;

notation
 let x be object;
 synonym x`3_3 for x`2;
end;

registration let x1,x2,x3;
 reduce [x1,x2,x3]`1_3 to x1;
 reducibility;
 reduce [x1,x2,x3]`2_3 to x2;
 reducibility;
 reduce [x1,x2,x3]`3_3 to x3;
 reducibility;
end;

registration let x be triple object;
 reduce [x`1_3,x`2_3,x`3_3] to x;
 reducibility
  proof
   consider x1,x2,x3 such that
A1:  x = [x1,x2,x3] by Def5;
   thus thesis by A1;
  end;
end;

theorem
 for a,b being triple object
   st a`1_3 = b`1_3 & a`2_3 = b`2_3 & a`3_3 = b`3_3
  holds a = b
proof let a,b be triple object such that
A1: a`1_3 = b`1_3 & a`2_3 = b`2_3 & a`3_3 = b`3_3;
  a = [a`1_3,a`2_3,a`3_3] & b = [b`1_3,b`2_3,b`3_3];
 hence a = b by A1;
end;

begin :: Quadruples

definition
  let x1,x2,x3,x4 be object;
  func [x1,x2,x3,x4] -> object equals
  [[x1,x2,x3],x4];
  coherence;
end;

definition let x;
 attr x is quadruple means
:Def9: ex x1,x2,x3,x4 st x = [x1,x2,x3,x4];
end;

registration let x1,x2,x3,x4;
 cluster [x1,x2,x3,x4] -> quadruple;
 coherence;
end;

theorem
 [x1,x2,x3,x4] = [y1,y2,y3,y4]
   implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4
proof
  assume
A1: [x1,x2,x3,x4] = [y1,y2,y3,y4];
  then [x1,x2,x3] = [y1,y2,y3] by Th1;
  hence thesis by A1,Th3,Th1;
end;

registration
 cluster quadruple for object;
 existence
 proof
  take [the object, the object, the object, the object],
    the object, the object, the object, the object;
  thus thesis;
 end;
 cluster quadruple -> triple for object;
 coherence
  proof let x be object;
   given x1,x2,x3,x4 such that
A1:  x = [x1,x2,x3,x4];
    x = [[x1,x2],x3,x4] by A1;
   hence thesis;
  end;
end;

definition
 let x be object;
  func x`1_4 -> object equals x`1`1`1;
   coherence;
  func x`2_4 -> object equals x`1`1`2;
  coherence;
end;

notation let x be object;
 synonym x`3_4 for x`2_3;
 synonym x`4_4 for x`2;
end;

registration let x1,x2,x3,x4;
 reduce [x1,x2,x3,x4]`1_4 to x1;
 reducibility;
 reduce [x1,x2,x3,x4]`2_4 to x2;
 reducibility;
 reduce [x1,x2,x3,x4]`3_4 to x3;
 reducibility;
 reduce [x1,x2,x3,x4]`4_4 to x4;
 reducibility;
end;

registration let x be quadruple object;
 reduce [x`1_4,x`2_4,x`3_4,x`4_4] to x;
 reducibility
  proof
   consider x1,x2,x3,x4 such that
A1:  x = [x1,x2,x3,x4] by Def9;
   thus thesis by A1;
  end;
end;

reserve X,X1,X2,X3,X4,Y for set;

:: Preliminaries

theorem Th6:
 [x,y] in X implies x 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 in {x} by TARSKI:def 1;
   hence x in union union X by A2,TARSKI:def 4;
  end;

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

:: Projections

definition
  let X be set;
  func proj1 X -> set means
:Def12:
  x in it iff ex y st [x,y] in X;
  existence
  proof
    defpred Q[object] means ex y st [$1,y] in X;
    consider Y such that
A1: for x being object holds x in Y iff x in union union X & Q[x]
       from XBOOLE_0:sch 1;
    take Y;
    let x;
    thus x in Y implies ex y st [x,y] in X by A1;
    given y such that
A2:  [x,y] in X;
    x in union union X by A2,Th6;
   hence thesis by A2,A1;
  end;
  uniqueness
  proof
    let X1,X2;
    assume that
A3: for x holds x in X1 iff ex y st [x,y] in X and
A4: for x holds x in X2 iff ex y st [x,y] in X;
    now
      let x be object;
      x in X1 iff ex y st [x,y] in X by A3;
      hence x in X1 iff x in X2 by A4;
    end;
    hence thesis by TARSKI:2;
  end;
  func proj2 X -> set means
:Def13:
  x in it iff ex y st [y,x] in X;
  existence
  proof
    defpred Q[object] means ex y st [y,$1] in X;
    consider Y such that
A5: for x being object holds x in Y iff x in union union X & Q[x]
      from XBOOLE_0:sch 1;
    take Y;
    let x;
    thus x in Y implies ex y st [y,x] in X by A5;
    given y such that
A6:  [y,x] in X;
    x in union union X by A6,Th7;
   hence thesis by A6,A5;
  end;
  uniqueness
  proof
    let X1,X2;
    assume that
A7: for x holds x in X1 iff ex y st [y,x] in X and
A8: for x holds x in X2 iff ex y st [y,x] in X;
    now
      let x be object;
      x in X1 iff ex y st [y,x] in X by A7;
      hence x in X1 iff x in X2 by A8;
    end;
    hence thesis by TARSKI:2;
  end;
end;

theorem Th8:
 X c= Y implies proj1 X c= proj1 Y
proof assume
A1: X c= Y;
 let x be object;
 assume x in proj1 X;
  then consider y such that
A2: [x,y] in X by Def12;
  [x,y] in Y by A1,A2;
 hence thesis by Def12;
end;

theorem Th9:
 X c= Y implies proj2 X c= proj2 Y
proof assume
A1: X c= Y;
 let x be object;
 assume x in proj2 X;
  then consider y such that
A2: [y,x] in X by Def13;
  [y,x] in Y by A1,A2;
 hence thesis by Def13;
end;

definition
  let X be set;
  func proj1_3 X -> set equals
   proj1 proj1 X;
  coherence;
  func proj2_3 X -> set equals
   proj2 proj1 X;
  coherence;
end;

notation let X be set;
 synonym proj3_3 X for proj2 X;
end;

theorem Th10:
 X c= Y implies proj1_3 X c= proj1_3 Y
proof assume X c= Y;
  then proj1 X c= proj1 Y by Th8;
 hence thesis by Th8;
end;

theorem Th11:
 X c= Y implies proj2_3 X c= proj2_3 Y
proof assume X c= Y;
  then proj1 X c= proj1 Y by Th8;
 hence thesis by Th9;
end;

theorem Th12:
 x in proj1_3 X implies ex y,z st [x,y,z] in X
proof assume x in proj1_3 X;
  then consider y such that
A1: [x,y] in proj1 X by Def12;
  consider z such that
A2: [[x,y],z] in X by A1,Def12;
 take y,z;
 thus thesis by A2;
end;

theorem Th13:
 [x,y,z] in X implies x in proj1_3 X
 proof
  assume [x,y,z] in X;
   then [x,y] in proj1 X by Def12;
  hence thesis by Def12;
 end;

theorem Th14:
 x in proj2_3 X implies ex y,z st [y,x,z] in X
proof assume x in proj2_3 X;
  then consider y such that
A1: [y,x] in proj1 X by Def13;
  consider z such that
A2: [[y,x],z] in X by A1,Def12;
 take y,z;
 thus thesis by A2;
end;

theorem Th15:
 [x,y,z] in X implies y in proj2_3 X
 proof
  assume [x,y,z] in X;
   then [x,y] in proj1 X by Def12;
  hence thesis by Def13;
 end;

definition
  let X be set;
func proj1_4 X -> set equals
   proj1 proj1_3 X;
  coherence;
  func proj2_4 X -> set equals
   proj2 proj1_3 X;
  coherence;
end;

notation let X be set;
  synonym proj3_4 X for proj2_3 X;
  synonym proj4_4 X for proj2 X;
end;

theorem Th16:
 X c= Y implies proj1_4 X c= proj1_4 Y
proof assume X c= Y;
  then proj1_3 X c= proj1_3 Y by Th10;
 hence thesis by Th8;
end;

theorem Th17:
 X c= Y implies proj2_4 X c= proj2_4 Y
proof assume X c= Y;
  then proj1_3 X c= proj1_3 Y by Th10;
 hence thesis by Th9;
end;

theorem Th18:
 x in proj1_4 X implies ex x1,x2,x3 st [x,x1,x2,x3] in X
proof assume x in proj1_4 X;
  then consider x1 such that
A1: [x,x1] in proj1_3 X by Def12;
  consider x2 such that
A2: [[x,x1],x2] in proj1 X by A1,Def12;
  consider x3 such that
A3: [[[x,x1],x2],x3] in X by A2,Def12;
 take x1,x2,x3;
 thus thesis by A3;
end;

theorem Th19:
 [x,x1,x2,x3] in X implies x in proj1_4 X
proof
 assume [x,x1,x2,x3] in X;
  then [[x,x1],x2,x3] in X;
  then [x,x1] in proj1_3 X by Th13;
 hence thesis by Def12;
end;

theorem Th20:
 x in proj2_4 X implies ex x1,x2,x3 st [x1,x,x2,x3] in X
proof assume x in proj2_4 X;
  then consider x1 such that
A1: [x1,x] in proj1_3 X by Def13;
  consider x2 such that
A2: [[x1,x],x2] in proj1 X by A1,Def12;
  consider x3 such that
A3: [[[x1,x],x2],x3] in X by A2,Def12;
 take x1,x2,x3;
 thus thesis by A3;
end;

theorem Th21:
 [x1,x,x2,x3] in X implies x in proj2_4 X
proof
 assume [x1,x,x2,x3] in X;
  then [[x1,x],x2,x3] in X;
  then [x1,x] in proj1_3 X by Th13;
 hence thesis by Def13;
end;

theorem
 for a,b being quadruple object
  st a`1_4 = b`1_4 & a`2_4 = b`2_4 & a`3_4 = b`3_4 & a`4_4 = b`4_4
  holds a = b
proof let a,b be quadruple object such that
A1: a`1_4 = b`1_4 & a`2_4 = b`2_4 & a`3_4 = b`3_4 & a`4_4 = b`4_4;
  a = [a`1_4,a`2_4,a`3_4,a`4_4] & b = [b`1_4,b`2_4,b`3_4,b`4_4];
 hence a = b by A1;
end;

begin :: Boolean properties

registration let X be empty set;
 cluster proj1 X -> empty;
 coherence
  proof
   assume proj1 X is non empty;
    then consider x being object such that
A1:   x in proj1 X;
    ex y st [x,y] in X by A1,Def12;
   hence contradiction;
  end;
end;

registration let X be empty set;
 cluster proj2 X -> empty;
 coherence
  proof
   assume proj2 X is non empty;
    then consider x being object such that
A1:   x in proj2 X;
    ex y st [y,x] in X by A1,Def13;
   hence contradiction;
  end;
end;

registration let X be empty set;
 cluster proj1_3 X -> empty;
 coherence;
end;

registration let X be empty set;
 cluster proj2_3 X -> empty;
 coherence;
end;

registration let X be empty set;
 cluster proj1_4 X -> empty;
 coherence;
end;

registration let X be empty set;
 cluster proj2_4 X -> empty;
 coherence;
end;

theorem Th23:
 proj1(X \/ Y) = proj1 X \/ proj1 Y
proof
  thus proj1(X \/ Y) c= proj1 X \/ proj1 Y
  proof
   let x be object;
   assume x in proj1(X \/ Y);
    then consider y such that
A1: [x,y] in X \/ Y by Def12;
    [x,y] in X or [x,y] in Y by A1,XBOOLE_0:def 3;
    then x in proj1 X or x in proj1 Y by Def12;
   hence thesis by XBOOLE_0:def 3;
  end;
A2: proj1 Y c= proj1(X \/ Y) by Th8,XBOOLE_1:7;
   proj1 X c= proj1(X \/ Y) by Th8,XBOOLE_1:7;
  hence proj1 X \/ proj1 Y c= proj1 (X \/ Y) by A2,XBOOLE_1:8;
end;

theorem
  proj1(X /\ Y) c= proj1 X /\ proj1 Y
proof
  proj1(X /\ Y) c= proj1 X & proj1(X /\ Y) c= proj1 Y by Th8,XBOOLE_1:17;
 hence thesis by XBOOLE_1:19;
end;

theorem Th25:
  proj1 X \ proj1 Y c= proj1(X \ Y)
proof
 let x be object;
 assume
A1: x in proj1 X \ proj1 Y;
  then x in proj1 X by XBOOLE_0:def 5;
  then consider y such that
A2: [x,y] in X by Def12;
  not x in proj1 Y by A1,XBOOLE_0:def 5;
  then not [x,y] in Y by Def12;
  then [x,y] in X \ Y by A2,XBOOLE_0:def 5;
 hence thesis by Def12;
end;

theorem
  proj1 X \+\ proj1 Y c= proj1(X \+\ Y)
proof
  proj1 X \ proj1 Y c= proj1(X \ Y) & proj1 Y \ proj1 X c= proj1(Y \ X)
     by Th25;
  then proj1 X \+\ proj1 Y c= proj1(X\Y) \/ proj1(Y\X) by XBOOLE_1:13;
 hence thesis by Th23;
end;

theorem Th27:
 proj2(X \/ Y) = proj2 X \/ proj2 Y
proof
 thus proj2(X \/ Y) c= proj2 X \/ proj2 Y
  proof
   let y be object;
   assume y in proj2(X \/ Y);
    then consider x such that
A1: [x,y] in X \/ Y by Def13;
    [x,y] in X or [x,y] in Y by A1,XBOOLE_0:def 3;
    then y in proj2 X or y in proj2 Y by Def13;
   hence thesis by XBOOLE_0:def 3;
  end;
A2: proj2 Y c= proj2(X \/ Y) by Th9,XBOOLE_1:7;
  proj2 X c= proj2(X \/ Y) by Th9,XBOOLE_1:7;
 hence proj2 X \/ proj2 Y c= proj2(X \/ Y) by A2,XBOOLE_1:8;
end;

theorem
  proj2(X /\ Y) c= proj2 X /\ proj2 Y
proof
  let y be object;
  assume y in proj2(X /\ Y);
  then consider x such that
A1: [x,y] in X /\ Y by Def13;
  [x,y] in Y by A1,XBOOLE_0:def 4;
  then
A2: y in proj2 Y by Def13;
  [x,y] in X by A1,XBOOLE_0:def 4;
  then y in proj2 X by Def13;
  hence thesis by A2,XBOOLE_0:def 4;
end;

theorem Th29:
  proj2 X \ proj2 Y c= proj2(X \ Y)
proof
  let y be object;
  assume
A1: y in proj2 X \ proj2 Y;
  then y in proj2 X by XBOOLE_0:def 5;
  then consider x such that
A2: [x,y] in X by Def13;
  not y in proj2 Y by A1,XBOOLE_0:def 5;
  then not [x,y] in Y by Def13;
  then [x,y] in X \ Y by A2,XBOOLE_0:def 5;
  hence thesis by Def13;
end;

theorem
   proj2 X \+\ proj2 Y c= proj2(X \+\ Y)
proof
  proj2 X \ proj2 Y c= proj2(X \ Y) & proj2 Y \ proj2 X c= proj2(Y \ X)
      by Th29;
  then proj2 X \+\ proj2 Y c= proj2(X\Y) \/ proj2(Y\X) by XBOOLE_1:13;
  hence thesis by Th27;
end;

theorem Th31:
 proj1_3(X \/ Y) = proj1_3 X \/ proj1_3 Y
proof
 thus proj1_3(X \/ Y) = proj1(proj1 X \/ proj1 Y) by Th23
     .= proj1_3 X \/ proj1_3 Y by Th23;
end;

theorem
  proj1_3(X /\ Y) c= proj1_3 X /\ proj1_3 Y
proof
  proj1_3(X /\ Y) c= proj1_3 X & proj1_3(X /\ Y) c= proj1_3 Y
       by Th10,XBOOLE_1:17;
 hence thesis by XBOOLE_1:19;
end;

theorem Th33:
  proj1_3 X \ proj1_3 Y c= proj1_3(X \ Y)
proof
 let x be object;
 assume
A1: x in proj1_3 X \ proj1_3 Y;
  then x in proj1_3 X by XBOOLE_0:def 5;
  then consider y,z such that
A2: [x,y,z] in X by Th12;
  not x in proj1_3 Y by A1,XBOOLE_0:def 5;
  then not [x,y,z] in Y by Th13;
  then [x,y,z] in X \ Y by A2,XBOOLE_0:def 5;
 hence thesis by Th13;
end;

theorem
  proj1_3 X \+\ proj1_3 Y c= proj1_3(X \+\ Y)
proof
  proj1_3 X \ proj1_3 Y c= proj1_3(X \ Y) &
  proj1_3 Y \ proj1_3 X c= proj1_3(Y \ X) by Th33;
  then proj1_3 X \+\ proj1_3 Y c= proj1_3(X\Y) \/ proj1_3(Y\X) by XBOOLE_1:13;
 hence thesis by Th31;
end;

theorem Th35:
 proj2_3(X \/ Y) = proj2_3 X \/ proj2_3 Y
proof
 thus proj2_3(X \/ Y) = proj2(proj1 X \/ proj1 Y) by Th23
     .= proj2_3 X \/ proj2_3 Y by Th27;
end;

theorem
  proj2_3(X /\ Y) c= proj2_3 X /\ proj2_3 Y
proof
  proj2_3(X /\ Y) c= proj2_3 X & proj2_3(X /\ Y) c= proj2_3 Y
   by Th11,XBOOLE_1:17;
 hence thesis by XBOOLE_1:19;
end;

theorem Th37:
  proj2_3 X \ proj2_3 Y c= proj2_3(X \ Y)
proof
 let x be object;
 assume
A1: x in proj2_3 X \ proj2_3 Y;
  then x in proj2_3 X by XBOOLE_0:def 5;
  then consider y,z such that
A2: [y,x,z] in X by Th14;
  not x in proj2_3 Y by A1,XBOOLE_0:def 5;
  then not [y,x,z] in Y by Th15;
  then [y,x,z] in X \ Y by A2,XBOOLE_0:def 5;
 hence thesis by Th15;
end;

theorem
  proj2_3 X \+\ proj2_3 Y c= proj2_3(X \+\ Y)
proof
  proj2_3 X \ proj2_3 Y c= proj2_3(X \ Y) &
  proj2_3 Y \ proj2_3 X c= proj2_3(Y \ X) by Th37;
  then proj2_3 X \+\ proj2_3 Y c= proj2_3(X\Y) \/ proj2_3(Y\X) by XBOOLE_1:13;
 hence thesis by Th35;
end;

theorem Th39:
 proj1_4(X \/ Y) = proj1_4 X \/ proj1_4 Y
proof
 thus proj1_4(X \/ Y) = proj1(proj1_3 X \/ proj1_3 Y) by Th31
     .= proj1_4 X \/ proj1_4 Y by Th23;
end;

theorem
  proj1_4(X /\ Y) c= proj1_4 X /\ proj1_4 Y
proof
  proj1_4(X /\ Y) c= proj1_4 X & proj1_4(X /\ Y) c= proj1_4 Y
   by Th16,XBOOLE_1:17;
 hence thesis by XBOOLE_1:19;
end;

theorem Th41:
  proj1_4 X \ proj1_4 Y c= proj1_4(X \ Y)
proof
 let x be object;
 assume
A1: x in proj1_4 X \ proj1_4 Y;
  then x in proj1_4 X by XBOOLE_0:def 5;
  then consider x1,x2,x3 such that
A2: [x,x1,x2,x3] in X by Th18;
  not x in proj1_4 Y by A1,XBOOLE_0:def 5;
  then not [x,x1,x2,x3] in Y by Th19;
  then [x,x1,x2,x3] in X \ Y by A2,XBOOLE_0:def 5;
 hence thesis by Th19;
end;

theorem
  proj1_4 X \+\ proj1_4 Y c= proj1_4(X \+\ Y)
proof
  proj1_4 X \ proj1_4 Y c= proj1_4(X \ Y) &
  proj1_4 Y \ proj1_4 X c= proj1_4(Y \ X) by Th41;
  then proj1_4 X \+\ proj1_4 Y c= proj1_4(X\Y) \/ proj1_4(Y\X) by XBOOLE_1:13;
 hence thesis by Th39;
end;

theorem Th43:
 proj2_4(X \/ Y) = proj2_4 X \/ proj2_4 Y
proof
 thus proj2_4(X \/ Y) = proj2(proj1_3 X \/ proj1_3 Y) by Th31
     .= proj2_4 X \/ proj2_4 Y by Th27;
end;

theorem
  proj2_4(X /\ Y) c= proj2_4 X /\ proj2_4 Y
proof
  proj2_4(X /\ Y) c= proj2_4 X & proj2_4(X /\ Y) c= proj2_4 Y
    by Th17,XBOOLE_1:17;
 hence thesis by XBOOLE_1:19;
end;

theorem Th45:
  proj2_4 X \ proj2_4 Y c= proj2_4(X \ Y)
proof
 let x be object;
 assume
A1: x in proj2_4 X \ proj2_4 Y;
  then x in proj2_4 X by XBOOLE_0:def 5;
  then consider x1,x2,x3 such that
A2: [x1,x,x2,x3] in X by Th20;
  not x in proj2_4 Y by A1,XBOOLE_0:def 5;
  then not [x1,x,x2,x3] in Y by Th21;
  then [x1,x,x2,x3] in X \ Y by A2,XBOOLE_0:def 5;
 hence thesis by Th21;
end;

theorem
  proj2_4 X \+\ proj2_4 Y c= proj2_4(X \+\ Y)
proof
  proj2_4 X \ proj2_4 Y c= proj2_4(X \ Y) &
  proj2_4 Y \ proj2_4 X c= proj2_4(Y \ X) by Th45;
  then proj2_4 X \+\ proj2_4 Y c= proj2_4(X\Y) \/ proj2_4(Y\X) by XBOOLE_1:13;
 hence thesis by Th43;
end;