pzfmisc1.miz



    begin

    reserve i for object,

I for set,

f for Function,

x,x1,x2,y,A,B,X,Y,Z for ManySortedSet of I;

    theorem :: PZFMISC1:1

    

     Th1: for X be object holds 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 :: PZFMISC1:2

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

    theorem :: PZFMISC1:3

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

    definition

      let I, A;

      :: PZFMISC1:def1

      func {A} -> ManySortedSet of I means

      : Def1: for i be 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 be object st i in I holds (X . i) = {(A . i)} and

         A2: for i be 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;

      :: PZFMISC1:def2

      func {A,B} -> ManySortedSet of I means

      : Def2: for i be 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 be 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 be object st i in I holds (X . i) = {(A . i), (B . i)} and

         A2: for i be 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 be object such that

         A2: i in I;

         {(A . i), (B . i)} is finite;

        hence thesis by A2, Def2;

      end;

    end

    theorem :: PZFMISC1:4

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

    (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 :: PZFMISC1:6

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

    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 :: PZFMISC1:8

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

    ( {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 :: PZFMISC1:11

     {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 :: PZFMISC1:12

     {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 :: PZFMISC1:13

     {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 :: PZFMISC1:14

     {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 :: PZFMISC1:15

     {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 :: PZFMISC1:16

     {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 :: PZFMISC1:17

    ( {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 :: PZFMISC1:18

    ( {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 :: PZFMISC1:19

    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 be 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 :: PZFMISC1:20

    ( {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 :: PZFMISC1:21

    ( {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 :: PZFMISC1:22

    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 be 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 :: PZFMISC1:23

    ( {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 :: PZFMISC1:24

    ( {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 :: PZFMISC1:25

     {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 :: PZFMISC1: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 :: PZFMISC1: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 :: PZFMISC1:28

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

     {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 :: PZFMISC1:30

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

    ( 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 :: PZFMISC1:32

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

     {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 :: PZFMISC1:34

     {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 :: PZFMISC1:35

    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

    theorem :: PZFMISC1:36

    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 :: PZFMISC1:37

    (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 :: PZFMISC1:38

    ( {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 :: PZFMISC1:39

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

    ( {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 :: PZFMISC1:41

    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 be 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 :: PZFMISC1:42

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

    theorem :: PZFMISC1:43

    (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 :: PZFMISC1:44

    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 :: PZFMISC1:45

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

    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 be 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 :: PZFMISC1:47

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

    theorem :: PZFMISC1:48

    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 :: PZFMISC1:49

    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 be 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 :: PZFMISC1:50

    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 be 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 :: PZFMISC1:51

    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 be 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 :: PZFMISC1:52

    ( {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 :: PZFMISC1:53

    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 be 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 :: PZFMISC1:54

    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 be 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 :: PZFMISC1:55

    ( {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 :: PZFMISC1:56

    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

    theorem :: PZFMISC1:57

    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 :: PZFMISC1:58

    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 :: PZFMISC1:59

     [|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 :: PZFMISC1:60

    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 :: PZFMISC1:61

    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 :: PZFMISC1:62

    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 :: PZFMISC1:63

     [|(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 :: PZFMISC1:64

     [|(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 :: PZFMISC1:65

     [|(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 :: PZFMISC1:66

     [|(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 :: PZFMISC1:67

    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 :: PZFMISC1:68

     [|(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 :: PZFMISC1:69

    ( [|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 :: PZFMISC1:70

    (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 :: PZFMISC1:71

    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 :: PZFMISC1:72

     [| {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 :: PZFMISC1:73

    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 :: PZFMISC1:74

    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 :: PZFMISC1:75

    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 :: PZFMISC1:76

     [|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 :: PZFMISC1:77

    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 :: PZFMISC1:78

    (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 :: PZFMISC1:79

    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 :: PZFMISC1:80

    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

    definition

      let I, A, B;

      :: PZFMISC1:def3

      pred A is_transformable_to B means for i be set st i in I holds (B . i) = {} implies (A . i) = {} ;

      reflexivity ;

    end