:: Kuratowski Pairs. {T}uples and Projections
:: by Grzegorz Bancerek, Artur Korni\l owicz and Andrzej Trybulec
::
:: Received December 9, 2011
:: Copyright (c) 2011-2018 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;