xtuple_0.miz

    begin

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

    definition

      let x be object;

      :: XTUPLE_0:def1

      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 :: XTUPLE_0:1



     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];

      :: XTUPLE_0:def2

      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;

      :: XTUPLE_0:def3

      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 :: XTUPLE_0:2

    for a,b be 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

    definition

      let x1,x2,x3 be object;

      :: XTUPLE_0:def4

      func [x1,x2,x3] -> object equals [ [x1, x2], x3];

      coherence ;

    end

    definition

      let x;

      :: XTUPLE_0:def5

      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 :: XTUPLE_0:3



     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;

      :: XTUPLE_0:def6

      func x `1_3 -> object equals ((x `1 ) `1 );

      coherence ;

      :: XTUPLE_0:def7

      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 :: XTUPLE_0:4

    for a,b be 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

    definition

      let x1,x2,x3,x4 be object;

      :: XTUPLE_0:def8

      func [x1,x2,x3,x4] -> object equals [ [x1, x2, x3], x4];

      coherence ;

    end

    definition

      let x;

      :: XTUPLE_0:def9

      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 :: XTUPLE_0:5

     [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;

      :: XTUPLE_0:def10

      func x `1_4 -> object equals (((x `1 ) `1 ) `1 );

      coherence ;

      :: XTUPLE_0:def11

      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;

    theorem :: XTUPLE_0:6



     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 :: XTUPLE_0:7



     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;

    definition

      let X be set;

      :: XTUPLE_0:def12

      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 be 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;

      :: XTUPLE_0:def13

      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 be 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 :: XTUPLE_0:8



     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 :: XTUPLE_0:9



     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;

      :: XTUPLE_0:def14

      func proj1_3 X -> set equals ( proj1 ( proj1 X));

      coherence ;

      :: XTUPLE_0:def15

      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 :: XTUPLE_0:10



     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 :: XTUPLE_0:11



     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 :: XTUPLE_0:12



     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 :: XTUPLE_0:13



     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 :: XTUPLE_0:14



     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 :: XTUPLE_0:15



     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;

      :: XTUPLE_0:def16

      func proj1_4 X -> set equals ( proj1 ( proj1_3 X));

      coherence ;

      :: XTUPLE_0:def17

      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 :: XTUPLE_0:16



     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 :: XTUPLE_0:17



     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 :: XTUPLE_0:18



     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 :: XTUPLE_0:19



     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 :: XTUPLE_0:20



     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 :: XTUPLE_0:21



     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 :: XTUPLE_0:22

    for a,b be 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

    registration

      let X be empty set;

      cluster ( proj1 X) -> empty;

      coherence

      proof

        assume ( proj1 X) is non empty;

        then

        consider x be 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 be 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 :: XTUPLE_0:23



     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 :: XTUPLE_0:24

    ( 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 :: XTUPLE_0:25



     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 :: XTUPLE_0:26

    (( 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 :: XTUPLE_0:27



     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 :: XTUPLE_0:28

    ( 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 :: XTUPLE_0:29



     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 :: XTUPLE_0:30

    (( 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 :: XTUPLE_0:31



     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 :: XTUPLE_0:32

    ( 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 :: XTUPLE_0:33



     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 :: XTUPLE_0:34

    (( 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 :: XTUPLE_0:35



     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 :: XTUPLE_0:36

    ( 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 :: XTUPLE_0:37



     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 :: XTUPLE_0:38

    (( 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 :: XTUPLE_0:39



     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 :: XTUPLE_0:40

    ( 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 :: XTUPLE_0:41



     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 :: XTUPLE_0:42

    (( 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 :: XTUPLE_0:43



     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 :: XTUPLE_0:44

    ( 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 :: XTUPLE_0:45



     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 :: XTUPLE_0:46

    (( 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;