pboole.miz



    begin

    reserve i,j,e,u for object;

    theorem :: PBOOLE:1

    for f be Function st f is non-empty holds ( rng f) is with_non-empty_elements;

    theorem :: PBOOLE:2

    for f be Function holds f is empty-yielding iff f = {} or ( rng f) = { {} }

    proof

      let f be Function;

      hereby

        assume that

         A1: f is empty-yielding and

         A2: f <> {} ;

        thus ( rng f) = { {} }

        proof

          thus for i be object st i in ( rng f) holds i in { {} } by A1;

          set e = the Element of ( dom f);

          let i be object;

          assume i in { {} };

          then

           A3: i = {} by TARSKI:def 1;

          

           A4: ( dom f) <> {} by A2;

          (f . e) is empty by A1;

          hence thesis by A4, A3, FUNCT_1:def 3;

        end;

      end;

      assume

       A5: f = {} or ( rng f) = { {} };

      per cases by A5;

        suppose f = {} ;

        hence for i be object st i in ( dom f) holds (f . i) is empty;

      end;

        suppose

         A6: ( rng f) = { {} };

        let i be object;

        assume i in ( dom f);

        then (f . i) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A6, TARSKI:def 1;

      end;

    end;

    reserve I for set;

    registration

      let I;

      cluster total for I -defined Function;

      existence

      proof

        take (I --> {} );

        thus thesis;

      end;

    end

    definition

      let I;

      mode ManySortedSet of I is totalI -defined Function;

    end

    reserve x,X,Y,Z,V for ManySortedSet of I;

    scheme :: PBOOLE:sch1

    KuratowskiFunction { A() -> set , F( object) -> set } :

ex f be ManySortedSet of A() st for e be object st e in A() holds (f . e) in F(e)

      provided

       A1: for e be object st e in A() holds F(e) <> {} ;

      defpred P[ object, object] means $2 in F($1);

       A2:

      now

        let e be object;

        set fe = the Element of F(e);

        assume

         A3: e in A();

        reconsider fe as object;

        take fe;

        F(e) <> {} by A1, A3;

        hence P[e, fe];

      end;

      consider f be Function such that

       A4: ( dom f) = A() and

       A5: for e be object st e in A() holds P[e, (f . e)] from CLASSES1:sch 1( A2);

      reconsider f as ManySortedSet of A() by A4, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      thus thesis by A5;

    end;

    definition

      let I, X, Y;

      :: PBOOLE:def1

      pred X in Y means for i be object st i in I holds (X . i) in (Y . i);

      :: PBOOLE:def2

      pred X c= Y means for i be object st i in I holds (X . i) c= (Y . i);

      reflexivity ;

    end

    definition

      let I be non empty set, X,Y be ManySortedSet of I;

      :: original: in

      redefine

      pred X in Y;

      asymmetry

      proof

        let X,Y be ManySortedSet of I;

        assume

         A1: for i be object st i in I holds (X . i) in (Y . i);

         not for i st i in I holds (Y . i) in (X . i)

        proof

          assume

           A2: for i st i in I holds (Y . i) in (X . i);

          consider i be object such that

           A3: i in I by XBOOLE_0:def 1;

          (X . i) in (Y . i) by A1, A3;

          hence thesis by A2, A3;

        end;

        hence thesis;

      end;

    end

    scheme :: PBOOLE:sch2

    PSeparation { I() -> set , A() -> ManySortedSet of I() , P[ object, object] } :

ex X be ManySortedSet of I() st for i be object st i in I() holds for e be object holds e in (X . i) iff e in (A() . i) & P[i, e];

      defpred R[ object, object] means ex A be set st A = $2 & for e be object holds e in A iff e in (A() . $1) & P[$1, e];

       A1:

      now

        let i be object such that i in I();

        defpred Q[ object] means P[i, $1];

        ex u be set st for e be object holds e in u iff e in (A() . i) & Q[e] from XBOOLE_0:sch 1;

        hence ex u be object st R[i, u];

      end;

      consider f be Function such that

       A2: ( dom f) = I() and

       A3: for i be object st i in I() holds R[i, (f . i)] from CLASSES1:sch 1( A1);

      reconsider f as ManySortedSet of I() by A2, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      let i be object;

      assume i in I();

      then R[i, (f . i)] by A3;

      hence thesis;

    end;

    theorem :: PBOOLE:3

    

     Th3: (for i be object st i in I holds (X . i) = (Y . i)) implies X = Y

    proof

      ( dom X) = I & ( dom Y) = I by PARTFUN1:def 2;

      hence thesis;

    end;

    definition

      let I;

      :: PBOOLE:def3

      func EmptyMS I -> ManySortedSet of I equals (I --> {} );

      coherence ;

      correctness ;

      let X, Y;

      :: PBOOLE:def4

      func X (\/) Y -> ManySortedSet of I means

      : Def4: for i be object st i in I holds (it . i) = ((X . i) \/ (Y . i));

      existence

      proof

        deffunc F( object) = ((X . $1) \/ (Y . $1));

        consider f be Function such that

         A1: ( dom f) = I and

         A2: for i be object st i in I holds (f . i) = F(i) from FUNCT_1:sch 3;

        f is ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let A1,A2 be ManySortedSet of I such that

         A3: for i be object st i in I holds (A1 . i) = ((X . i) \/ (Y . i)) and

         A4: for i be object st i in I holds (A2 . i) = ((X . i) \/ (Y . i));

        now

          let i be object;

          assume

           A5: i in I;

          

          hence (A1 . i) = ((X . i) \/ (Y . i)) by A3

          .= (A2 . i) by A4, A5;

        end;

        hence thesis by Th3;

      end;

      commutativity ;

      idempotence ;

      :: PBOOLE:def5

      func X (/\) Y -> ManySortedSet of I means

      : Def5: for i be object st i in I holds (it . i) = ((X . i) /\ (Y . i));

      existence

      proof

        deffunc F( object) = ((X . $1) /\ (Y . $1));

        consider f be Function such that

         A6: ( dom f) = I and

         A7: for i be object st i in I holds (f . i) = F(i) from FUNCT_1:sch 3;

        f is ManySortedSet of I by A6, PARTFUN1:def 2, RELAT_1:def 18;

        hence thesis by A7;

      end;

      uniqueness

      proof

        let A1,A2 be ManySortedSet of I such that

         A8: for i be object st i in I holds (A1 . i) = ((X . i) /\ (Y . i)) and

         A9: for i be object st i in I holds (A2 . i) = ((X . i) /\ (Y . i));

        now

          let i be object;

          assume

           A10: i in I;

          

          hence (A1 . i) = ((X . i) /\ (Y . i)) by A8

          .= (A2 . i) by A9, A10;

        end;

        hence thesis by Th3;

      end;

      commutativity ;

      idempotence ;

      :: PBOOLE:def6

      func X (\) Y -> ManySortedSet of I means

      : Def6: for i be object st i in I holds (it . i) = ((X . i) \ (Y . i));

      existence

      proof

        deffunc F( object) = ((X . $1) \ (Y . $1));

        consider f be Function such that

         A11: ( dom f) = I and

         A12: for i be object st i in I holds (f . i) = F(i) from FUNCT_1:sch 3;

        f is ManySortedSet of I by A11, PARTFUN1:def 2, RELAT_1:def 18;

        hence thesis by A12;

      end;

      uniqueness

      proof

        let A1,A2 be ManySortedSet of I such that

         A13: for i be object st i in I holds (A1 . i) = ((X . i) \ (Y . i)) and

         A14: for i be object st i in I holds (A2 . i) = ((X . i) \ (Y . i));

        now

          let i be object;

          assume

           A15: i in I;

          

          hence (A1 . i) = ((X . i) \ (Y . i)) by A13

          .= (A2 . i) by A14, A15;

        end;

        hence thesis by Th3;

      end;

      :: PBOOLE:def7

      pred X overlaps Y means for i be object st i in I holds (X . i) meets (Y . i);

      symmetry ;

      :: PBOOLE:def8

      pred X misses Y means for i be object st i in I holds (X . i) misses (Y . i);

      symmetry ;

    end

    notation

      let I;

      let X, Y;

      antonym X meets Y for X misses Y;

    end

    definition

      let I, X, Y;

      :: PBOOLE:def9

      func X (\+\) Y -> ManySortedSet of I equals ((X (\) Y) (\/) (Y (\) X));

      correctness ;

      commutativity ;

    end

    theorem :: PBOOLE:4

    

     Th4: for i st i in I holds ((X (\+\) Y) . i) = ((X . i) \+\ (Y . i))

    proof

      let i such that

       A1: i in I;

      

      thus ((X (\+\) Y) . i) = (((X (\) Y) . i) \/ ((Y (\) X) . i)) by A1, Def4

      .= (((X . i) \ (Y . i)) \/ ((Y (\) X) . i)) by A1, Def6

      .= ((X . i) \+\ (Y . i)) by A1, Def6;

    end;

    theorem :: PBOOLE:5

    for i be object holds (( EmptyMS I) . i) = {} ;

    theorem :: PBOOLE:6

    

     Th6: (for i be object st i in I holds (X . i) = {} ) implies X = ( EmptyMS I)

    proof

      assume

       A1: for i be object st i in I holds (X . i) = {} ;

      now

        let i be object;

        assume i in I;

        

        hence (X . i) = {} by A1

        .= (( EmptyMS I) . i);

      end;

      hence thesis by Th3;

    end;

    theorem :: PBOOLE:7

    

     Th7: x in X or x in Y implies x in (X (\/) Y)

    proof

      assume

       A1: x in X or x in Y;

      let i be object;

      assume

       A2: i in I;

      then (x . i) in (X . i) or (x . i) in (Y . i) by A1;

      then (x . i) in ((X . i) \/ (Y . i)) by XBOOLE_0:def 3;

      hence thesis by A2, Def4;

    end;

    theorem :: PBOOLE:8

    

     Th8: x in (X (/\) Y) iff x in X & x in Y

    proof

      hereby

        assume

         A1: x in (X (/\) Y);

        thus x in X

        proof

          let i be object;

          assume

           A2: i in I;

          then (x . i) in ((X (/\) Y) . i) by A1;

          then (x . i) in ((X . i) /\ (Y . i)) by A2, Def5;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus x in Y

        proof

          let i be object;

          assume

           A3: i in I;

          then (x . i) in ((X (/\) Y) . i) by A1;

          then (x . i) in ((X . i) /\ (Y . i)) by A3, Def5;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A4: x in X & x in Y;

      let i be object;

      assume

       A5: i in I;

      then (x . i) in (X . i) & (x . i) in (Y . i) by A4;

      then (x . i) in ((X . i) /\ (Y . i)) by XBOOLE_0:def 4;

      hence thesis by A5, Def5;

    end;

    theorem :: PBOOLE:9

    

     Th9: x in X & X c= Y implies x in Y

    proof

      assume

       A1: x in X & X c= Y;

      let i be object;

      assume i in I;

      then (x . i) in (X . i) & (X . i) c= (Y . i) by A1;

      hence thesis;

    end;

    theorem :: PBOOLE:10

    

     Th10: x in X & x in Y implies X overlaps Y

    proof

      assume

       A1: x in X & x in Y;

      let i be object;

      assume i in I;

      then (x . i) in (X . i) & (x . i) in (Y . i) by A1;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: PBOOLE:11

    

     Th11: X overlaps Y implies ex x st x in X & x in Y

    proof

      deffunc F( object) = ((X . $1) /\ (Y . $1));

      assume

       A1: X overlaps Y;

      

       A2: for i be object st i in I holds F(i) <> {} by XBOOLE_0:def 7, A1;

      consider x be ManySortedSet of I such that

       A3: for i be object st i in I holds (x . i) in F(i) from KuratowskiFunction( A2);

      take x;

      now

        let i be object;

        assume i in I;

        then (x . i) in ((X . i) /\ (Y . i)) by A3;

        hence (x . i) in (X . i) by XBOOLE_0:def 4;

      end;

      hence x in X;

      now

        let i be object;

        assume i in I;

        then (x . i) in ((X . i) /\ (Y . i)) by A3;

        hence (x . i) in (Y . i) by XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:12

    x in (X (\) Y) implies x in X

    proof

      assume

       A1: x in (X (\) Y);

      thus x in X

      proof

        let i be object;

        assume

         A2: i in I;

        then (x . i) in ((X (\) Y) . i) by A1;

        then (x . i) in ((X . i) \ (Y . i)) by A2, Def6;

        hence thesis;

      end;

    end;

    begin

    

     Lm1: X c= Y & Y c= X implies X = Y

    proof

      assume X c= Y & Y c= X;

      then for i be object st i in I holds (X . i) = (Y . i);

      hence thesis by Th3;

    end;

    definition

      let I, X, Y;

      :: original: =

      redefine

      :: PBOOLE:def10

      pred X = Y means for i be object st i in I holds (X . i) = (Y . i);

      compatibility by Th3;

    end

    theorem :: PBOOLE:13

    

     Th13: X c= Y & Y c= Z implies X c= Z

    proof

      assume that

       A1: X c= Y and

       A2: Y c= Z;

      let i be object such that

       A3: i in I;

      let e be object;

      assume

       A4: e in (X . i);

      (X . i) c= (Y . i) by A1, A3;

      then

       A5: e in (Y . i) by A4;

      (Y . i) c= (Z . i) by A2, A3;

      hence thesis by A5;

    end;

    theorem :: PBOOLE:14

    

     Th14: X c= (X (\/) Y)

    proof

      let i be object such that

       A1: i in I;

      let e be object;

      assume e in (X . i);

      then e in ((X . i) \/ (Y . i)) by XBOOLE_0:def 3;

      hence thesis by A1, Def4;

    end;

    theorem :: PBOOLE:15

    

     Th15: (X (/\) Y) c= X

    proof

      let i be object such that

       A1: i in I;

      let e be object;

      assume e in ((X (/\) Y) . i);

      then e in ((X . i) /\ (Y . i)) by A1, Def5;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: PBOOLE:16

    

     Th16: X c= Z & Y c= Z implies (X (\/) Y) c= Z

    proof

      assume

       A1: X c= Z & Y c= Z;

      let i be object;

      assume

       A2: i in I;

      then (X . i) c= (Z . i) & (Y . i) c= (Z . i) by A1;

      then ((X . i) \/ (Y . i)) c= (Z . i) by XBOOLE_1: 8;

      hence thesis by A2, Def4;

    end;

    theorem :: PBOOLE:17

    

     Th17: Z c= X & Z c= Y implies Z c= (X (/\) Y)

    proof

      assume

       A1: Z c= X & Z c= Y;

      let i be object;

      assume

       A2: i in I;

      then (Z . i) c= (X . i) & (Z . i) c= (Y . i) by A1;

      then (Z . i) c= ((X . i) /\ (Y . i)) by XBOOLE_1: 19;

      hence thesis by A2, Def5;

    end;

    theorem :: PBOOLE:18

    X c= Y implies (X (\/) Z) c= (Y (\/) Z)

    proof

      assume

       A1: X c= Y;

      

       A2: Z c= (Y (\/) Z) by Th14;

      Y c= (Y (\/) Z) by Th14;

      then X c= (Y (\/) Z) by A1, Th13;

      hence (X (\/) Z) c= (Y (\/) Z) by A2, Th16;

    end;

    theorem :: PBOOLE:19

    

     Th19: X c= Y implies (X (/\) Z) c= (Y (/\) Z)

    proof

      assume

       A1: X c= Y;

      

       A2: (X (/\) Z) c= Z by Th15;

      (X (/\) Z) c= X by Th15;

      then (X (/\) Z) c= Y by A1, Th13;

      hence (X (/\) Z) c= (Y (/\) Z) by A2, Th17;

    end;

    theorem :: PBOOLE:20

    

     Th20: X c= Y & Z c= V implies (X (\/) Z) c= (Y (\/) V)

    proof

      assume that

       A1: X c= Y and

       A2: Z c= V;

      V c= (Y (\/) V) by Th14;

      then

       A3: Z c= (Y (\/) V) by A2, Th13;

      Y c= (Y (\/) V) by Th14;

      then X c= (Y (\/) V) by A1, Th13;

      hence thesis by A3, Th16;

    end;

    theorem :: PBOOLE:21

    X c= Y & Z c= V implies (X (/\) Z) c= (Y (/\) V)

    proof

      assume that

       A1: X c= Y and

       A2: Z c= V;

      (X (/\) Z) c= Z by Th15;

      then

       A3: (X (/\) Z) c= V by A2, Th13;

      (X (/\) Z) c= X by Th15;

      then (X (/\) Z) c= Y by A1, Th13;

      hence thesis by A3, Th17;

    end;

    theorem :: PBOOLE:22

    

     Th22: X c= Y implies (X (\/) Y) = Y

    proof

      assume X c= Y;

      then

       A1: (X (\/) Y) c= Y by Th16;

      Y c= (X (\/) Y) by Th14;

      hence thesis by A1, Lm1;

    end;

    theorem :: PBOOLE:23

    

     Th23: X c= Y implies (X (/\) Y) = X

    proof

      assume

       A1: X c= Y;

      

       A2: (X (/\) Y) c= X by Th15;

      X c= (X (/\) Y) by A1, Th17;

      hence thesis by A2, Lm1;

    end;

    theorem :: PBOOLE:24

    (X (/\) Y) c= (X (\/) Z)

    proof

      (X (/\) Y) c= X & X c= (X (\/) Z) by Th14, Th15;

      hence thesis by Th13;

    end;

    theorem :: PBOOLE:25

    X c= Z implies (X (\/) (Y (/\) Z)) = ((X (\/) Y) (/\) Z)

    proof

      assume

       A1: X c= Z;

      let i be object;

      assume

       A2: i in I;

      then

       A3: (X . i) c= (Z . i) by A1;

      

      thus ((X (\/) (Y (/\) Z)) . i) = ((X . i) \/ ((Y (/\) Z) . i)) by A2, Def4

      .= ((X . i) \/ ((Y . i) /\ (Z . i))) by A2, Def5

      .= (((X . i) \/ (Y . i)) /\ (Z . i)) by A3, XBOOLE_1: 30

      .= (((X (\/) Y) . i) /\ (Z . i)) by A2, Def4

      .= (((X (\/) Y) (/\) Z) . i) by A2, Def5;

    end;

    theorem :: PBOOLE:26

    X = (Y (\/) Z) iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V

    proof

      thus X = (Y (\/) Z) implies Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V by Th14, Th16;

      assume that

       A1: Y c= X & Z c= X and

       A2: Y c= V & Z c= V implies X c= V;

      Y c= (Y (\/) Z) & Z c= (Y (\/) Z) by Th14;

      then

       A3: X c= (Y (\/) Z) by A2;

      (Y (\/) Z) c= X by A1, Th16;

      hence thesis by A3, Lm1;

    end;

    theorem :: PBOOLE:27

    X = (Y (/\) Z) iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X

    proof

      thus X = (Y (/\) Z) implies X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X by Th15, Th17;

      assume that

       A1: X c= Y & X c= Z and

       A2: V c= Y & V c= Z implies V c= X;

      

       A3: X c= (Y (/\) Z) by A1, Th17;

      (Y (/\) Z) c= Y & (Y (/\) Z) c= Z implies (Y (/\) Z) c= X by A2;

      hence thesis by A3, Lm1, Th15;

    end;

    theorem :: PBOOLE:28

    

     Th28: ((X (\/) Y) (\/) Z) = (X (\/) (Y (\/) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence (((X (\/) Y) (\/) Z) . i) = (((X (\/) Y) . i) \/ (Z . i)) by Def4

      .= (((X . i) \/ (Y . i)) \/ (Z . i)) by A1, Def4

      .= ((X . i) \/ ((Y . i) \/ (Z . i))) by XBOOLE_1: 4

      .= ((X . i) \/ ((Y (\/) Z) . i)) by A1, Def4

      .= ((X (\/) (Y (\/) Z)) . i) by A1, Def4;

    end;

    theorem :: PBOOLE:29

    

     Th29: ((X (/\) Y) (/\) Z) = (X (/\) (Y (/\) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence (((X (/\) Y) (/\) Z) . i) = (((X (/\) Y) . i) /\ (Z . i)) by Def5

      .= (((X . i) /\ (Y . i)) /\ (Z . i)) by A1, Def5

      .= ((X . i) /\ ((Y . i) /\ (Z . i))) by XBOOLE_1: 16

      .= ((X . i) /\ ((Y (/\) Z) . i)) by A1, Def5

      .= ((X (/\) (Y (/\) Z)) . i) by A1, Def5;

    end;

    theorem :: PBOOLE:30

    

     Th30: (X (/\) (X (\/) Y)) = X

    proof

      X c= (X (\/) Y) by Th14;

      then

       A1: X c= (X (/\) (X (\/) Y)) by Th17;

      (X (/\) (X (\/) Y)) c= X by Th15;

      hence (X (/\) (X (\/) Y)) = X by A1, Lm1;

    end;

    theorem :: PBOOLE:31

    

     Th31: (X (\/) (X (/\) Y)) = X

    proof

      (X (/\) Y) c= X by Th15;

      then

       A1: (X (\/) (X (/\) Y)) c= X by Th16;

      X c= (X (\/) (X (/\) Y)) by Th14;

      hence (X (\/) (X (/\) Y)) = X by A1, Lm1;

    end;

    theorem :: PBOOLE:32

    

     Th32: (X (/\) (Y (\/) Z)) = ((X (/\) Y) (\/) (X (/\) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence ((X (/\) (Y (\/) Z)) . i) = ((X . i) /\ ((Y (\/) Z) . i)) by Def5

      .= ((X . i) /\ ((Y . i) \/ (Z . i))) by A1, Def4

      .= (((X . i) /\ (Y . i)) \/ ((X . i) /\ (Z . i))) by XBOOLE_1: 23

      .= (((X (/\) Y) . i) \/ ((X . i) /\ (Z . i))) by A1, Def5

      .= (((X (/\) Y) . i) \/ ((X (/\) Z) . i)) by A1, Def5

      .= (((X (/\) Y) (\/) (X (/\) Z)) . i) by A1, Def4;

    end;

    theorem :: PBOOLE:33

    

     Th33: (X (\/) (Y (/\) Z)) = ((X (\/) Y) (/\) (X (\/) Z))

    proof

      

      thus (X (\/) (Y (/\) Z)) = ((X (\/) (X (/\) Z)) (\/) (Y (/\) Z)) by Th31

      .= (X (\/) ((X (/\) Z) (\/) (Y (/\) Z))) by Th28

      .= (X (\/) ((X (\/) Y) (/\) Z)) by Th32

      .= (((X (\/) Y) (/\) X) (\/) ((X (\/) Y) (/\) Z)) by Th30

      .= ((X (\/) Y) (/\) (X (\/) Z)) by Th32;

    end;

    theorem :: PBOOLE:34

    ((X (/\) Y) (\/) (X (/\) Z)) = X implies X c= (Y (\/) Z)

    proof

      assume ((X (/\) Y) (\/) (X (/\) Z)) = X;

      then X = (X (/\) (Y (\/) Z)) by Th32;

      hence thesis by Th15;

    end;

    theorem :: PBOOLE:35

    ((X (\/) Y) (/\) (X (\/) Z)) = X implies (Y (/\) Z) c= X

    proof

      assume ((X (\/) Y) (/\) (X (\/) Z)) = X;

      then X = (X (\/) (Y (/\) Z)) by Th33;

      hence thesis by Th14;

    end;

    theorem :: PBOOLE:36

    (((X (/\) Y) (\/) (Y (/\) Z)) (\/) (Z (/\) X)) = (((X (\/) Y) (/\) (Y (\/) Z)) (/\) (Z (\/) X))

    proof

      

      thus (((X (/\) Y) (\/) (Y (/\) Z)) (\/) (Z (/\) X)) = ((((X (/\) Y) (\/) (Y (/\) Z)) (\/) Z) (/\) (((X (/\) Y) (\/) (Y (/\) Z)) (\/) X)) by Th33

      .= (((X (/\) Y) (\/) ((Y (/\) Z) (\/) Z)) (/\) (((X (/\) Y) (\/) (Y (/\) Z)) (\/) X)) by Th28

      .= (((X (/\) Y) (\/) Z) (/\) (((X (/\) Y) (\/) (Y (/\) Z)) (\/) X)) by Th31

      .= (((X (/\) Y) (\/) Z) (/\) (((X (/\) Y) (\/) X) (\/) (Y (/\) Z))) by Th28

      .= (((X (/\) Y) (\/) Z) (/\) (X (\/) (Y (/\) Z))) by Th31

      .= (((X (\/) Z) (/\) (Y (\/) Z)) (/\) (X (\/) (Y (/\) Z))) by Th33

      .= (((X (\/) Z) (/\) (Y (\/) Z)) (/\) ((X (\/) Y) (/\) (X (\/) Z))) by Th33

      .= ((X (\/) Y) (/\) (((Y (\/) Z) (/\) (X (\/) Z)) (/\) (X (\/) Z))) by Th29

      .= ((X (\/) Y) (/\) ((Y (\/) Z) (/\) ((X (\/) Z) (/\) (X (\/) Z)))) by Th29

      .= (((X (\/) Y) (/\) (Y (\/) Z)) (/\) (Z (\/) X)) by Th29;

    end;

    theorem :: PBOOLE:37

    (X (\/) Y) c= Z implies X c= Z

    proof

      X c= (X (\/) Y) by Th14;

      hence thesis by Th13;

    end;

    theorem :: PBOOLE:38

    X c= (Y (/\) Z) implies X c= Y

    proof

      (Y (/\) Z) c= Y by Th15;

      hence thesis by Th13;

    end;

    theorem :: PBOOLE:39

    ((X (\/) Y) (\/) Z) = ((X (\/) Z) (\/) (Y (\/) Z))

    proof

      

      thus ((X (\/) Y) (\/) Z) = (X (\/) (Y (\/) (Z (\/) Z))) by Th28

      .= (X (\/) ((Z (\/) Y) (\/) Z)) by Th28

      .= ((X (\/) Z) (\/) (Y (\/) Z)) by Th28;

    end;

    theorem :: PBOOLE:40

    ((X (/\) Y) (/\) Z) = ((X (/\) Z) (/\) (Y (/\) Z))

    proof

      

      thus ((X (/\) Y) (/\) Z) = (X (/\) (Y (/\) (Z (/\) Z))) by Th29

      .= (X (/\) ((Z (/\) Y) (/\) Z)) by Th29

      .= ((X (/\) Z) (/\) (Y (/\) Z)) by Th29;

    end;

    theorem :: PBOOLE:41

    (X (\/) (X (\/) Y)) = (X (\/) Y)

    proof

      

      thus (X (\/) (X (\/) Y)) = ((X (\/) X) (\/) Y) by Th28

      .= (X (\/) Y);

    end;

    theorem :: PBOOLE:42

    (X (/\) (X (/\) Y)) = (X (/\) Y)

    proof

      

      thus (X (/\) (X (/\) Y)) = ((X (/\) X) (/\) Y) by Th29

      .= (X (/\) Y);

    end;

    begin

    theorem :: PBOOLE:43

    

     Th43: ( EmptyMS I) c= X

    proof

      let i be object such that i in I;

      let e be object;

      assume e in (( EmptyMS I) . i);

      hence thesis;

    end;

    theorem :: PBOOLE:44

    

     Th44: X c= ( EmptyMS I) implies X = ( EmptyMS I)

    proof

      assume X c= ( EmptyMS I);

      then X c= ( EmptyMS I) & ( EmptyMS I) c= X by Th43;

      hence thesis by Lm1;

    end;

    theorem :: PBOOLE:45

    X c= Y & X c= Z & (Y (/\) Z) = ( EmptyMS I) implies X = ( EmptyMS I) by Th17, Th44;

    theorem :: PBOOLE:46

    X c= Y & (Y (/\) Z) = ( EmptyMS I) implies (X (/\) Z) = ( EmptyMS I) by Th44, Th19;

    theorem :: PBOOLE:47

    (X (\/) ( EmptyMS I)) = X & (( EmptyMS I) (\/) X) = X by Th22, Th43;

    theorem :: PBOOLE:48

    (X (\/) Y) = ( EmptyMS I) implies X = ( EmptyMS I) by Th44, Th14;

    theorem :: PBOOLE:49

    (X (/\) ( EmptyMS I)) = ( EmptyMS I) by Th23, Th43;

    theorem :: PBOOLE:50

    X c= (Y (\/) Z) & (X (/\) Z) = ( EmptyMS I) implies X c= Y

    proof

      assume that

       A1: X c= (Y (\/) Z) and

       A2: (X (/\) Z) = ( EmptyMS I);

      (X (/\) (Y (\/) Z)) = X by A1, Th23;

      then ((Y (/\) X) (\/) ( EmptyMS I)) = X by A2, Th32;

      then (Y (/\) X) = X by Th22, Th43;

      hence thesis by Th15;

    end;

    theorem :: PBOOLE:51

    Y c= X & (X (/\) Y) = ( EmptyMS I) implies Y = ( EmptyMS I) by Th23;

    begin

    theorem :: PBOOLE:52

    

     Th52: (X (\) Y) = ( EmptyMS I) iff X c= Y

    proof

      hereby

        assume

         A1: (X (\) Y) = ( EmptyMS I);

        now

          let i be object;

          assume i in I;

          

          then ((X . i) \ (Y . i)) = ((X (\) Y) . i) by Def6

          .= {} by A1;

          hence (X . i) c= (Y . i) by XBOOLE_1: 37;

        end;

        hence X c= Y;

      end;

      assume

       A2: X c= Y;

      now

        let i be object;

        assume

         A3: i in I;

        then

         A4: (X . i) c= (Y . i) by A2;

        

        thus ((X (\) Y) . i) = ((X . i) \ (Y . i)) by A3, Def6

        .= {} by A4, XBOOLE_1: 37;

      end;

      hence thesis by Th6;

    end;

    theorem :: PBOOLE:53

    

     Th53: X c= Y implies (X (\) Z) c= (Y (\) Z)

    proof

      assume

       A1: X c= Y;

      now

        let i be object;

        assume

         A2: i in I;

        then

         A3: ((X (\) Z) . i) = ((X . i) \ (Z . i)) & ((Y (\) Z) . i) = ((Y . i) \ (Z . i)) by Def6;

        (X . i) c= (Y . i) by A1, A2;

        hence ((X (\) Z) . i) c= ((Y (\) Z) . i) by A3, XBOOLE_1: 33;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:54

    

     Th54: X c= Y implies (Z (\) Y) c= (Z (\) X)

    proof

      assume

       A1: X c= Y;

      now

        let i be object;

        assume

         A2: i in I;

        then

         A3: ((Z (\) X) . i) = ((Z . i) \ (X . i)) & ((Z (\) Y) . i) = ((Z . i) \ (Y . i)) by Def6;

        (X . i) c= (Y . i) by A1, A2;

        hence ((Z (\) Y) . i) c= ((Z (\) X) . i) by A3, XBOOLE_1: 34;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:55

    X c= Y & Z c= V implies (X (\) V) c= (Y (\) Z)

    proof

      assume X c= Y & Z c= V;

      then (X (\) V) c= (Y (\) V) & (Y (\) V) c= (Y (\) Z) by Th53, Th54;

      hence thesis by Th13;

    end;

    theorem :: PBOOLE:56

    

     Th56: (X (\) Y) c= X

    proof

      now

        let i be object such that

         A1: i in I;

        ((X . i) \ (Y . i)) c= (X . i);

        hence ((X (\) Y) . i) c= (X . i) by A1, Def6;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:57

    X c= (Y (\) X) implies X = ( EmptyMS I)

    proof

      assume

       A1: X c= (Y (\) X);

      let i be object;

      assume

       A2: i in I;

      then (X . i) c= ((Y (\) X) . i) by A1;

      then (X . i) c= ((Y . i) \ (X . i)) by A2, Def6;

      

      hence (X . i) = {} by XBOOLE_1: 38

      .= (( EmptyMS I) . i);

    end;

    theorem :: PBOOLE:58

    (X (\) X) = ( EmptyMS I) by Th52;

    theorem :: PBOOLE:59

    

     Th59: (X (\) ( EmptyMS I)) = X

    proof

      let i be object;

      assume i in I;

      

      hence ((X (\) ( EmptyMS I)) . i) = ((X . i) \ (( EmptyMS I) . i)) by Def6

      .= ((X . i) \ {} )

      .= (X . i);

    end;

    theorem :: PBOOLE:60

    

     Th60: (( EmptyMS I) (\) X) = ( EmptyMS I) by Th43, Th52;

    theorem :: PBOOLE:61

    (X (\) (X (\/) Y)) = ( EmptyMS I) by Th14, Th52;

    theorem :: PBOOLE:62

    

     Th62: (X (/\) (Y (\) Z)) = ((X (/\) Y) (\) Z)

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence ((X (/\) (Y (\) Z)) . i) = ((X . i) /\ ((Y (\) Z) . i)) by Def5

      .= ((X . i) /\ ((Y . i) \ (Z . i))) by A1, Def6

      .= (((X . i) /\ (Y . i)) \ (Z . i)) by XBOOLE_1: 49

      .= (((X (/\) Y) . i) \ (Z . i)) by A1, Def5

      .= (((X (/\) Y) (\) Z) . i) by A1, Def6;

    end;

    theorem :: PBOOLE:63

    

     Th63: ((X (\) Y) (/\) Y) = ( EmptyMS I)

    proof

      

       A1: (Y (/\) X) c= Y by Th15;

      

      thus ((X (\) Y) (/\) Y) = ((Y (/\) X) (\) Y) by Th62

      .= ( EmptyMS I) by A1, Th52;

      thus thesis;

    end;

    theorem :: PBOOLE:64

    

     Th64: (X (\) (Y (\) Z)) = ((X (\) Y) (\/) (X (/\) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence ((X (\) (Y (\) Z)) . i) = ((X . i) \ ((Y (\) Z) . i)) by Def6

      .= ((X . i) \ ((Y . i) \ (Z . i))) by A1, Def6

      .= (((X . i) \ (Y . i)) \/ ((X . i) /\ (Z . i))) by XBOOLE_1: 52

      .= (((X . i) \ (Y . i)) \/ ((X (/\) Z) . i)) by A1, Def5

      .= (((X (\) Y) . i) \/ ((X (/\) Z) . i)) by A1, Def6

      .= (((X (\) Y) (\/) (X (/\) Z)) . i) by A1, Def4;

    end;

    theorem :: PBOOLE:65

    

     Th65: ((X (\) Y) (\/) (X (/\) Y)) = X

    proof

      

      thus ((X (\) Y) (\/) (X (/\) Y)) = (X (\) (Y (\) Y)) by Th64

      .= (X (\) ( EmptyMS I)) by Th52

      .= X by Th59;

    end;

    theorem :: PBOOLE:66

    X c= Y implies Y = (X (\/) (Y (\) X))

    proof

      assume

       A1: X c= Y;

      

      thus Y = ((Y (\) X) (\/) (Y (/\) X)) by Th65

      .= (X (\/) (Y (\) X)) by A1, Th23;

    end;

    theorem :: PBOOLE:67

    

     Th67: (X (\/) (Y (\) X)) = (X (\/) Y)

    proof

      

      thus (X (\/) (Y (\) X)) = ((X (\/) (Y (/\) X)) (\/) (Y (\) X)) by Th31

      .= (X (\/) ((Y (/\) X) (\/) (Y (\) X))) by Th28

      .= (X (\/) Y) by Th65;

    end;

    theorem :: PBOOLE:68

    

     Th68: (X (\) (X (\) Y)) = (X (/\) Y)

    proof

      

      thus (X (\) (X (\) Y)) = ((X (\) X) (\/) (X (/\) Y)) by Th64

      .= (( EmptyMS I) (\/) (X (/\) Y)) by Th52

      .= (X (/\) Y) by Th22, Th43;

    end;

    theorem :: PBOOLE:69

    

     Th69: (X (\) (Y (/\) Z)) = ((X (\) Y) (\/) (X (\) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence ((X (\) (Y (/\) Z)) . i) = ((X . i) \ ((Y (/\) Z) . i)) by Def6

      .= ((X . i) \ ((Y . i) /\ (Z . i))) by A1, Def5

      .= (((X . i) \ (Y . i)) \/ ((X . i) \ (Z . i))) by XBOOLE_1: 54

      .= (((X . i) \ (Y . i)) \/ ((X (\) Z) . i)) by A1, Def6

      .= (((X (\) Y) . i) \/ ((X (\) Z) . i)) by A1, Def6

      .= (((X (\) Y) (\/) (X (\) Z)) . i) by A1, Def4;

    end;

    theorem :: PBOOLE:70

    

     Th70: (X (\) (X (/\) Y)) = (X (\) Y)

    proof

      

      thus (X (\) (X (/\) Y)) = ((X (\) X) (\/) (X (\) Y)) by Th69

      .= (( EmptyMS I) (\/) (X (\) Y)) by Th52

      .= (X (\) Y) by Th22, Th43;

    end;

    theorem :: PBOOLE:71

    (X (/\) Y) = ( EmptyMS I) iff (X (\) Y) = X

    proof

      hereby

        assume

         A1: (X (/\) Y) = ( EmptyMS I);

        

        thus (X (\) Y) = (X (\) (X (/\) Y)) by Th70

        .= X by A1, Th59;

      end;

      thus thesis by Th63;

    end;

    theorem :: PBOOLE:72

    

     Th72: ((X (\/) Y) (\) Z) = ((X (\) Z) (\/) (Y (\) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence (((X (\/) Y) (\) Z) . i) = (((X (\/) Y) . i) \ (Z . i)) by Def6

      .= (((X . i) \/ (Y . i)) \ (Z . i)) by A1, Def4

      .= (((X . i) \ (Z . i)) \/ ((Y . i) \ (Z . i))) by XBOOLE_1: 42

      .= (((X . i) \ (Z . i)) \/ ((Y (\) Z) . i)) by A1, Def6

      .= (((X (\) Z) . i) \/ ((Y (\) Z) . i)) by A1, Def6

      .= (((X (\) Z) (\/) (Y (\) Z)) . i) by A1, Def4;

    end;

    theorem :: PBOOLE:73

    

     Th73: ((X (\) Y) (\) Z) = (X (\) (Y (\/) Z))

    proof

      let i be object;

      assume

       A1: i in I;

      

      hence (((X (\) Y) (\) Z) . i) = (((X (\) Y) . i) \ (Z . i)) by Def6

      .= (((X . i) \ (Y . i)) \ (Z . i)) by A1, Def6

      .= ((X . i) \ ((Y . i) \/ (Z . i))) by XBOOLE_1: 41

      .= ((X . i) \ ((Y (\/) Z) . i)) by A1, Def4

      .= ((X (\) (Y (\/) Z)) . i) by A1, Def6;

    end;

    theorem :: PBOOLE:74

    ((X (/\) Y) (\) Z) = ((X (\) Z) (/\) (Y (\) Z))

    proof

      

       A1: (X (\) Z) c= X by Th56;

      

      thus ((X (/\) Y) (\) Z) = ((X (\) Z) (/\) Y) by Th62

      .= ((X (\) Z) (\) ((X (\) Z) (\) Y)) by Th68

      .= ((X (\) Z) (\) (X (\) (Z (\/) Y))) by Th73

      .= (((X (\) Z) (\) X) (\/) ((X (\) Z) (/\) (Z (\/) Y))) by Th64

      .= (( EmptyMS I) (\/) ((X (\) Z) (/\) (Z (\/) Y))) by A1, Th52

      .= ((X (\) Z) (/\) (Y (\/) Z)) by Th22, Th43

      .= ((X (\) Z) (/\) ((Y (\) Z) (\/) Z)) by Th67

      .= (((X (\) Z) (/\) (Y (\) Z)) (\/) ((X (\) Z) (/\) Z)) by Th32

      .= (((X (\) Z) (/\) (Y (\) Z)) (\/) ( EmptyMS I)) by Th63

      .= ((X (\) Z) (/\) (Y (\) Z)) by Th22, Th43;

    end;

    theorem :: PBOOLE:75

    

     Th75: ((X (\/) Y) (\) Y) = (X (\) Y)

    proof

      

      thus ((X (\/) Y) (\) Y) = ((X (\) Y) (\/) (Y (\) Y)) by Th72

      .= ((X (\) Y) (\/) ( EmptyMS I)) by Th52

      .= (X (\) Y) by Th22, Th43;

    end;

    theorem :: PBOOLE:76

    X c= (Y (\/) Z) implies (X (\) Y) c= Z & (X (\) Z) c= Y

    proof

      assume

       A1: X c= (Y (\/) Z);

      then (X (\) Y) c= ((Z (\/) Y) (\) Y) by Th53;

      then

       A2: (X (\) Y) c= (Z (\) Y) by Th75;

      (Z (\) Y) c= Z by Th56;

      hence (X (\) Y) c= Z by A2, Th13;

      (X (\) Z) c= ((Y (\/) Z) (\) Z) by A1, Th53;

      then

       A3: (X (\) Z) c= (Y (\) Z) by Th75;

      (Y (\) Z) c= Y by Th56;

      hence thesis by A3, Th13;

    end;

    theorem :: PBOOLE:77

    

     Th77: ((X (\/) Y) (\) (X (/\) Y)) = ((X (\) Y) (\/) (Y (\) X))

    proof

      

      thus ((X (\/) Y) (\) (X (/\) Y)) = ((X (\) (X (/\) Y)) (\/) (Y (\) (X (/\) Y))) by Th72

      .= ((X (\) Y) (\/) (Y (\) (X (/\) Y))) by Th70

      .= ((X (\) Y) (\/) (Y (\) X)) by Th70;

    end;

    theorem :: PBOOLE:78

    

     Th78: ((X (\) Y) (\) Y) = (X (\) Y)

    proof

      

      thus ((X (\) Y) (\) Y) = (X (\) (Y (\/) Y)) by Th73

      .= (X (\) Y);

    end;

    theorem :: PBOOLE:79

    (X (\) (Y (\/) Z)) = ((X (\) Y) (/\) (X (\) Z))

    proof

      

      thus (X (\) (Y (\/) Z)) = ((X (\) Y) (\) Z) by Th73

      .= (((X (\) Y) (/\) X) (\) Z) by Th56, Th23

      .= ((X (\) Y) (/\) (X (\) Z)) by Th62;

    end;

    theorem :: PBOOLE:80

    (X (\) Y) = (Y (\) X) implies X = Y

    proof

      assume (X (\) Y) = (Y (\) X);

      

      hence X = ((Y (\) X) (\/) (Y (/\) X)) by Th65

      .= Y by Th65;

    end;

    theorem :: PBOOLE:81

    (X (/\) (Y (\) Z)) = ((X (/\) Y) (\) (X (/\) Z))

    proof

      

       A1: (X (/\) Y) c= X by Th15;

      ((X (/\) Y) (\) (X (/\) Z)) = (((X (/\) Y) (\) X) (\/) ((X (/\) Y) (\) Z)) by Th69

      .= (( EmptyMS I) (\/) ((X (/\) Y) (\) Z)) by A1, Th52

      .= ((X (/\) Y) (\) Z) by Th22, Th43;

      hence thesis by Th62;

    end;

    theorem :: PBOOLE:82

    (X (\) Y) c= Z implies X c= (Y (\/) Z)

    proof

      assume

       A1: (X (\) Y) c= Z;

      (X (/\) Y) c= Y by Th15;

      then ((X (/\) Y) (\/) (X (\) Y)) c= (Y (\/) Z) by A1, Th20;

      hence thesis by Th65;

    end;

    theorem :: PBOOLE:83

    (X (\) Y) c= (X (\+\) Y) by Th14;

    theorem :: PBOOLE:84

    (X (\+\) ( EmptyMS I)) = X

    proof

      

      thus (X (\+\) ( EmptyMS I)) = (X (\/) (( EmptyMS I) (\) X)) by Th59

      .= (X (\/) ( EmptyMS I)) by Th60

      .= X by Th22, Th43;

    end;

    theorem :: PBOOLE:85

    (X (\+\) X) = ( EmptyMS I) by Th52;

    theorem :: PBOOLE:86

    (X (\/) Y) = ((X (\+\) Y) (\/) (X (/\) Y))

    proof

      

      thus (X (\/) Y) = (((X (\) Y) (\/) (X (/\) Y)) (\/) Y) by Th65

      .= ((X (\) Y) (\/) ((X (/\) Y) (\/) Y)) by Th28

      .= ((X (\) Y) (\/) Y) by Th31

      .= ((X (\) Y) (\/) ((Y (\) X) (\/) (Y (/\) X))) by Th65

      .= ((X (\+\) Y) (\/) (X (/\) Y)) by Th28;

    end;

    theorem :: PBOOLE:87

    

     Th87: (X (\+\) Y) = ((X (\/) Y) (\) (X (/\) Y))

    proof

      

      thus (X (\+\) Y) = ((X (\) (X (/\) Y)) (\/) (Y (\) X)) by Th70

      .= ((X (\) (X (/\) Y)) (\/) (Y (\) (X (/\) Y))) by Th70

      .= ((X (\/) Y) (\) (X (/\) Y)) by Th72;

    end;

    theorem :: PBOOLE:88

    ((X (\+\) Y) (\) Z) = ((X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z)))

    proof

      

      thus ((X (\+\) Y) (\) Z) = (((X (\) Y) (\) Z) (\/) ((Y (\) X) (\) Z)) by Th72

      .= ((X (\) (Y (\/) Z)) (\/) ((Y (\) X) (\) Z)) by Th73

      .= ((X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z))) by Th73;

    end;

    theorem :: PBOOLE:89

    (X (\) (Y (\+\) Z)) = ((X (\) (Y (\/) Z)) (\/) ((X (/\) Y) (/\) Z))

    proof

      

      thus (X (\) (Y (\+\) Z)) = (X (\) ((Y (\/) Z) (\) (Y (/\) Z))) by Th87

      .= ((X (\) (Y (\/) Z)) (\/) (X (/\) (Y (/\) Z))) by Th64

      .= ((X (\) (Y (\/) Z)) (\/) ((X (/\) Y) (/\) Z)) by Th29;

    end;

    theorem :: PBOOLE:90

    

     Th90: ((X (\+\) Y) (\+\) Z) = (X (\+\) (Y (\+\) Z))

    proof

      set S1 = (X (\) (Y (\/) Z)), S2 = (Y (\) (X (\/) Z)), S3 = (Z (\) (X (\/) Y)), S4 = ((X (/\) Y) (/\) Z);

      

      thus ((X (\+\) Y) (\+\) Z) = ((((X (\) Y) (\) Z) (\/) ((Y (\) X) (\) Z)) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X)))) by Th72

      .= ((S1 (\/) ((Y (\) X) (\) Z)) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X)))) by Th73

      .= ((S1 (\/) S2) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X)))) by Th73

      .= ((S1 (\/) S2) (\/) (Z (\) ((X (\/) Y) (\) (X (/\) Y)))) by Th77

      .= ((S1 (\/) S2) (\/) (S4 (\/) S3)) by Th64

      .= (((S1 (\/) S2) (\/) S4) (\/) S3) by Th28

      .= (((S1 (\/) S4) (\/) S2) (\/) S3) by Th28

      .= ((S1 (\/) S4) (\/) (S2 (\/) S3)) by Th28

      .= ((S1 (\/) (X (/\) (Y (/\) Z))) (\/) (S2 (\/) S3)) by Th29

      .= ((X (\) ((Y (\/) Z) (\) (Y (/\) Z))) (\/) (S2 (\/) S3)) by Th64

      .= ((X (\) ((Y (\) Z) (\/) (Z (\) Y))) (\/) (S2 (\/) (Z (\) (Y (\/) X)))) by Th77

      .= ((X (\) ((Y (\) Z) (\/) (Z (\) Y))) (\/) ((Y (\) (Z (\/) X)) (\/) ((Z (\) Y) (\) X))) by Th73

      .= ((X (\) ((Y (\) Z) (\/) (Z (\) Y))) (\/) (((Y (\) Z) (\) X) (\/) ((Z (\) Y) (\) X))) by Th73

      .= (X (\+\) (Y (\+\) Z)) by Th72;

    end;

    theorem :: PBOOLE:91

    (X (\) Y) c= Z & (Y (\) X) c= Z implies (X (\+\) Y) c= Z by Th16;

    theorem :: PBOOLE:92

    

     Th92: (X (\/) Y) = (X (\+\) (Y (\) X))

    proof

      

      thus (X (\/) Y) = (Y (\/) (X (\/) X))

      .= ((X (\/) Y) (\/) X) by Th28

      .= (((X (\) Y) (\/) Y) (\/) X) by Th67

      .= ((X (\) Y) (\/) (X (\/) Y)) by Th28

      .= ((X (\) Y) (\/) (X (\/) (Y (\) X))) by Th67

      .= (((X (\) Y) (\/) (X (/\) X)) (\/) (Y (\) X)) by Th28

      .= ((X (\) (Y (\) X)) (\/) (Y (\) X)) by Th64

      .= (X (\+\) (Y (\) X)) by Th78;

    end;

    theorem :: PBOOLE:93

    

     Th93: (X (/\) Y) = (X (\+\) (X (\) Y))

    proof

      

       A1: (X (\) Y) c= X by Th56;

      

      thus (X (/\) Y) = (X (\) (X (\) Y)) by Th68

      .= ((X (\) (X (\) Y)) (\/) ( EmptyMS I)) by Th22, Th43

      .= (X (\+\) (X (\) Y)) by A1, Th52;

    end;

    theorem :: PBOOLE:94

    

     Th94: (X (\) Y) = (X (\+\) (X (/\) Y))

    proof

      

       A1: (X (/\) Y) c= X by Th15;

      

      thus (X (\) Y) = (X (\) (X (/\) Y)) by Th70

      .= ((X (\) (X (/\) Y)) (\/) ( EmptyMS I)) by Th22, Th43

      .= (X (\+\) (X (/\) Y)) by A1, Th52;

    end;

    theorem :: PBOOLE:95

    

     Th95: (Y (\) X) = (X (\+\) (X (\/) Y))

    proof

      

       A1: X c= (Y (\/) X) by Th14;

      

      thus (Y (\) X) = ((Y (\/) X) (\) X) by Th75

      .= (( EmptyMS I) (\/) ((Y (\/) X) (\) X)) by Th22, Th43

      .= (X (\+\) (X (\/) Y)) by A1, Th52;

    end;

    theorem :: PBOOLE:96

    (X (\/) Y) = ((X (\+\) Y) (\+\) (X (/\) Y))

    proof

      

      thus (X (\/) Y) = (X (\+\) (Y (\) X)) by Th92

      .= (X (\+\) (Y (\+\) (X (/\) Y))) by Th94

      .= ((X (\+\) Y) (\+\) (X (/\) Y)) by Th90;

    end;

    theorem :: PBOOLE:97

    (X (/\) Y) = ((X (\+\) Y) (\+\) (X (\/) Y))

    proof

      

      thus (X (/\) Y) = (X (\+\) (X (\) Y)) by Th93

      .= (X (\+\) (Y (\+\) (X (\/) Y))) by Th95

      .= ((X (\+\) Y) (\+\) (X (\/) Y)) by Th90;

    end;

    begin

    theorem :: PBOOLE:98

    X overlaps Y or X overlaps Z implies X overlaps (Y (\/) Z)

    proof

      assume

       A1: X overlaps Y or X overlaps Z;

      per cases by A1;

        suppose X overlaps Y;

        then

        consider x such that

         A2: x in X and

         A3: x in Y by Th11;

        x in (Y (\/) Z) by A3, Th7;

        hence thesis by A2, Th10;

      end;

        suppose X overlaps Z;

        then

        consider x such that

         A4: x in X and

         A5: x in Z by Th11;

        x in (Y (\/) Z) by A5, Th7;

        hence thesis by A4, Th10;

      end;

    end;

    theorem :: PBOOLE:99

    

     Th99: X overlaps Y & Y c= Z implies X overlaps Z

    proof

      assume that

       A1: X overlaps Y and

       A2: Y c= Z;

      consider x such that

       A3: x in X and

       A4: x in Y by A1, Th11;

      x in Z by A2, A4, Th9;

      hence thesis by A3, Th10;

    end;

    theorem :: PBOOLE:100

    

     Th100: X overlaps Y & X c= Z implies Z overlaps Y

    proof

      assume that

       A1: X overlaps Y and

       A2: X c= Z;

      consider x such that

       A3: x in X and

       A4: x in Y by A1, Th11;

      x in Z by A2, A3, Th9;

      hence thesis by A4, Th10;

    end;

    theorem :: PBOOLE:101

    

     Th101: X c= Y & Z c= V & X overlaps Z implies Y overlaps V

    proof

      assume that

       A1: X c= Y and

       A2: Z c= V;

      assume X overlaps Z;

      then Y overlaps Z by A1, Th100;

      hence thesis by A2, Th99;

    end;

    theorem :: PBOOLE:102

    X overlaps (Y (/\) Z) implies X overlaps Y & X overlaps Z

    proof

      assume X overlaps (Y (/\) Z);

      then

      consider x such that

       A1: x in X and

       A2: x in (Y (/\) Z) by Th11;

      x in Y & x in Z by A2, Th8;

      hence thesis by A1, Th10;

    end;

    theorem :: PBOOLE:103

    X overlaps Z & X c= V implies X overlaps (Z (/\) V)

    proof

      assume that

       A1: X overlaps Z and

       A2: X c= V;

      consider x such that

       A3: x in X and

       A4: x in Z by A1, Th11;

      x in V by A2, A3, Th9;

      then x in (Z (/\) V) by A4, Th8;

      hence thesis by A3, Th10;

    end;

    theorem :: PBOOLE:104

    X overlaps (Y (\) Z) implies X overlaps Y by Th56, Th99;

    theorem :: PBOOLE:105

     not Y overlaps Z implies not (X (/\) Y) overlaps (X (/\) Z)

    proof

      assume

       A1: not Y overlaps Z;

      (X (/\) Y) c= Y & (X (/\) Z) c= Z by Th15;

      hence thesis by A1, Th101;

    end;

    theorem :: PBOOLE:106

    X overlaps (Y (\) Z) implies Y overlaps (X (\) Z)

    proof

      assume

       A1: X overlaps (Y (\) Z);

      let i be object;

      assume

       A2: i in I;

      then (X . i) meets ((Y (\) Z) . i) by A1;

      then (X . i) meets ((Y . i) \ (Z . i)) by A2, Def6;

      then (Y . i) meets ((X . i) \ (Z . i)) by XBOOLE_1: 81;

      hence thesis by A2, Def6;

    end;

    theorem :: PBOOLE:107

    

     Th107: X meets Y & Y c= Z implies X meets Z

    proof

      assume that

       A1: X meets Y and

       A2: Y c= Z;

      consider i be object such that

       A3: i in I and

       A4: (X . i) meets (Y . i) by A1;

      take i;

      (Y . i) c= (Z . i) by A2, A3;

      hence thesis by A3, A4, XBOOLE_1: 63;

    end;

    theorem :: PBOOLE:108

    

     Th108: Y misses (X (\) Y)

    proof

      now

        let i be object;

        assume i in I;

        then ((X (\) Y) . i) = ((X . i) \ (Y . i)) by Def6;

        hence (Y . i) misses ((X (\) Y) . i) by XBOOLE_1: 79;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:109

    (X (/\) Y) misses (X (\) Y)

    proof

      (X (/\) Y) c= Y & (X (\) Y) misses Y by Th15, Th108;

      hence thesis by Th107;

    end;

    theorem :: PBOOLE:110

    (X (/\) Y) misses (X (\+\) Y)

    proof

      now

        let i be object;

        assume i in I;

        then ((X (/\) Y) . i) = ((X . i) /\ (Y . i)) & ((X (\+\) Y) . i) = ((X . i) \+\ (Y . i)) by Def5, Th4;

        hence ((X (/\) Y) . i) misses ((X (\+\) Y) . i) by XBOOLE_1: 103;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:111

    

     Th111: X misses Y implies (X (/\) Y) = ( EmptyMS I)

    proof

      assume

       A1: X misses Y;

      now

        let i be object;

        assume

         A2: i in I;

        then

         A3: (X . i) misses (Y . i) by A1;

        

        thus ((X (/\) Y) . i) = ((X . i) /\ (Y . i)) by A2, Def5

        .= {} by A3;

      end;

      hence thesis by Th6;

    end;

    theorem :: PBOOLE:112

    X <> ( EmptyMS I) implies X meets X

    proof

      X = (X (/\) X);

      hence thesis by Th111;

    end;

    theorem :: PBOOLE:113

    X c= Y & X c= Z & Y misses Z implies X = ( EmptyMS I)

    proof

      assume

       A1: X c= Y & X c= Z;

      assume Y misses Z;

      then (Y (/\) Z) = ( EmptyMS I) by Th111;

      hence thesis by A1, Th17, Th44;

    end;

    theorem :: PBOOLE:114

    (Z (\/) V) = (X (\/) Y) & X misses Z & Y misses V implies X = V & Y = Z

    proof

      assume

       A1: (Z (\/) V) = (X (\/) Y);

      assume X misses Z & Y misses V;

      then

       A2: (X (/\) Z) = ( EmptyMS I) & (Y (/\) V) = ( EmptyMS I) by Th111;

      

      thus X = (X (/\) (Z (\/) V)) by Th23, A1, Th14

      .= ((X (/\) Z) (\/) (X (/\) V)) by Th32

      .= ((X (\/) Y) (/\) V) by A2, Th32

      .= V by A1, Th14, Th23;

      

      thus Y = (Y (/\) (Z (\/) V)) by Th23, A1, Th14

      .= ((Y (/\) Z) (\/) (Y (/\) V)) by Th32

      .= ((X (\/) Y) (/\) Z) by A2, Th32

      .= Z by A1, Th14, Th23;

    end;

    theorem :: PBOOLE:115

    

     Th115: X misses Y implies (X (\) Y) = X

    proof

      assume

       A1: X misses Y;

      let i be object;

      assume

       A2: i in I;

      then

       A3: ((X (\) Y) . i) = ((X . i) \ (Y . i)) by Def6;

      (X . i) misses (Y . i) by A1, A2;

      hence ((X (\) Y) . i) = (X . i) by A3, XBOOLE_1: 83;

    end;

    theorem :: PBOOLE:116

    X misses Y implies ((X (\/) Y) (\) Y) = X

    proof

      ((X (\/) Y) (\) Y) = (X (\) Y) by Th75;

      hence thesis by Th115;

    end;

    theorem :: PBOOLE:117

    (X (\) Y) = X implies X misses Y

    proof

      assume

       A1: (X (\) Y) = X;

      let i be object;

      assume i in I;

      then ((X . i) \ (Y . i)) = (X . i) by A1, Def6;

      hence thesis by XBOOLE_1: 83;

    end;

    theorem :: PBOOLE:118

    (X (\) Y) misses (Y (\) X)

    proof

      let i be object;

      assume i in I;

      then ((X (\) Y) . i) = ((X . i) \ (Y . i)) & ((Y (\) X) . i) = ((Y . i) \ (X . i)) by Def6;

      hence thesis by XBOOLE_1: 82;

    end;

    begin

    definition

      let I, X, Y;

      :: PBOOLE:def11

      pred X [= Y means for x st x in X holds x in Y;

      reflexivity ;

    end

    theorem :: PBOOLE:119

    X c= Y implies X [= Y

    proof

      assume

       A1: X c= Y;

      let x such that

       A2: x in X;

      let i be object;

      assume

       A3: i in I;

      then

       A4: (X . i) c= (Y . i) by A1;

      (x . i) in (X . i) by A2, A3;

      hence thesis by A4;

    end;

    theorem :: PBOOLE:120

    X [= Y & Y [= Z implies X [= Z;

    begin

    theorem :: PBOOLE:121

    ( EmptyMS {} ) in ( EmptyMS {} );

    theorem :: PBOOLE:122

    for X be ManySortedSet of {} holds X = {} ;

    reserve I for non empty set,

x,X,Y for ManySortedSet of I;

    theorem :: PBOOLE:123

    X overlaps Y implies X meets Y

    proof

      set i = the Element of I;

      assume X overlaps Y;

      then (X . i) meets (Y . i);

      hence thesis;

    end;

    theorem :: PBOOLE:124

    

     Th124: not ex x st x in ( EmptyMS I)

    proof

      set i = the Element of I;

      given x such that

       A1: x in ( EmptyMS I);

      (x . i) in (( EmptyMS I) . i) by A1;

      hence contradiction;

    end;

    theorem :: PBOOLE:125

    x in X & x in Y implies (X (/\) Y) <> ( EmptyMS I) by Th8, Th124;

    theorem :: PBOOLE:126

     not X overlaps ( EmptyMS I)

    proof

      assume X overlaps ( EmptyMS I);

      then ex x st x in X & x in ( EmptyMS I) by Th11;

      hence contradiction by Th124;

    end;

    theorem :: PBOOLE:127

    

     Th127: (X (/\) Y) = ( EmptyMS I) implies not X overlaps Y

    proof

      assume

       A1: (X (/\) Y) = ( EmptyMS I);

      assume X overlaps Y;

      then

      consider x such that

       A2: x in X & x in Y by Th11;

      x in (X (/\) Y) by A2, Th8;

      hence contradiction by A1, Th124;

    end;

    theorem :: PBOOLE:128

    X overlaps X implies X <> ( EmptyMS I)

    proof

      X = (X (/\) X);

      hence thesis by Th127;

    end;

    begin

    reserve I for set,

x,X,Y,Z for ManySortedSet of I;

    definition

      let I be set;

      let X be ManySortedSet of I;

      :: original: empty-yielding

      redefine

      :: PBOOLE:def12

      attr X is empty-yielding means for i be object st i in I holds (X . i) is empty;

      compatibility

      proof

        ( dom X) = I by PARTFUN1:def 2;

        hence thesis;

      end;

      :: original: non-empty

      redefine

      :: PBOOLE:def13

      attr X is non-empty means

      : Def13: for i be object st i in I holds (X . i) is non empty;

      compatibility

      proof

        ( dom X) = I by PARTFUN1:def 2;

        hence thesis;

      end;

    end

    registration

      let I be set;

      cluster empty-yielding for ManySortedSet of I;

      existence

      proof

        take ( EmptyMS I);

        let i be object;

        assume i in I;

        thus thesis;

      end;

      cluster non-empty for ManySortedSet of I;

      existence

      proof

        set e = the set;

        reconsider M = (I --> {e}) as ManySortedSet of I;

        take M;

        let i be object;

        assume i in I;

        hence thesis by FUNCOP_1: 7;

      end;

    end

    registration

      let I be non empty set;

      cluster non-empty -> non empty-yielding for ManySortedSet of I;

      coherence

      proof

        set i = the Element of I;

        let M be ManySortedSet of I;

        assume

         A1: M is non-empty;

        take i;

        thus i in I;

        thus thesis by A1;

      end;

      cluster empty-yielding -> non non-empty for ManySortedSet of I;

      coherence ;

    end

    theorem :: PBOOLE:129

    X is empty-yielding iff X = ( EmptyMS I)

    proof

      hereby

        assume X is empty-yielding;

        then for i be object st i in I holds (X . i) = {} ;

        hence X = ( EmptyMS I) by Th6;

      end;

      assume

       A1: X = ( EmptyMS I);

      let i be object;

      assume i in I;

      thus thesis by A1;

    end;

    theorem :: PBOOLE:130

    Y is empty-yielding & X c= Y implies X is empty-yielding

    proof

      assume

       A1: Y is empty-yielding & X c= Y;

      let i be object;

      assume i in I;

      then (X . i) c= (Y . i) & (Y . i) is empty by A1;

      hence thesis;

    end;

    theorem :: PBOOLE:131

    

     Th131: X is non-empty & X c= Y implies Y is non-empty

    proof

      assume

       A1: X is non-empty & X c= Y;

      let i be object;

      assume i in I;

      then (X . i) c= (Y . i) & (X . i) is non empty by A1;

      hence thesis;

    end;

    theorem :: PBOOLE:132

    

     Th132: X is non-empty & X [= Y implies X c= Y

    proof

      assume that

       A1: X is non-empty and

       A2: X [= Y;

      deffunc F( object) = (X . $1);

      

       A3: for i be object st i in I holds F(i) <> {} by A1;

      consider f be ManySortedSet of I such that

       A4: for i be object st i in I holds (f . i) in F(i) from KuratowskiFunction( A3);

      let i be object such that

       A5: i in I;

      let e be object;

      deffunc G( object) = ( IFEQ (i,$1,e,(f . $1)));

      consider g be Function such that

       A6: ( dom g) = I and

       A7: for u be object st u in I holds (g . u) = G(u) from FUNCT_1:sch 3;

      reconsider g as ManySortedSet of I by A6, PARTFUN1:def 2, RELAT_1:def 18;

      

       A8: (g . i) = ( IFEQ (i,i,e,(f . i))) by A5, A7

      .= e by FUNCOP_1:def 8;

      assume

       A9: e in (X . i);

      g in X

      proof

        let u be object such that

         A10: u in I;

        per cases ;

          suppose u = i;

          hence thesis by A8, A9;

        end;

          suppose

           A11: u <> i;

          (g . u) = ( IFEQ (i,u,e,(f . u))) by A7, A10

          .= (f . u) by A11, FUNCOP_1:def 8;

          hence thesis by A4, A10;

        end;

      end;

      then g in Y by A2;

      hence thesis by A5, A8;

    end;

    theorem :: PBOOLE:133

    X is non-empty & X [= Y implies Y is non-empty

    proof

      assume

       A1: X is non-empty;

      assume X [= Y;

      then X c= Y by A1, Th132;

      hence thesis by A1, Th131;

    end;

    reserve X for non-empty ManySortedSet of I;

    theorem :: PBOOLE:134

    ex x st x in X

    proof

      deffunc F( object) = (X . $1);

      

       A1: for i be object st i in I holds F(i) <> {} by Def13;

      consider f be ManySortedSet of I such that

       A2: for i be object st i in I holds (f . i) in F(i) from KuratowskiFunction( A1);

      take f;

      let i be object;

      thus thesis by A2;

    end;

    theorem :: PBOOLE:135

    

     Th135: (for x holds x in X iff x in Y) implies X = Y

    proof

      deffunc F( object) = (X . $1);

      

       A1: for i be object st i in I holds F(i) <> {} by Def13;

      consider f be ManySortedSet of I such that

       A2: for i be object st i in I holds (f . i) in F(i) from KuratowskiFunction( A1);

      assume

       A3: for x holds x in X iff x in Y;

      now

        let i be object such that

         A4: i in I;

        now

          let e be object;

          deffunc G( object) = ( IFEQ (i,$1,e,(f . $1)));

          consider g be Function such that

           A5: ( dom g) = I and

           A6: for u be object st u in I holds (g . u) = G(u) from FUNCT_1:sch 3;

          reconsider g as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;

          

           A7: (g . i) = ( IFEQ (i,i,e,(f . i))) by A4, A6

          .= e by FUNCOP_1:def 8;

          hereby

            assume

             A8: e in (X . i);

            g in X

            proof

              let u be object such that

               A9: u in I;

              per cases ;

                suppose u = i;

                hence thesis by A7, A8;

              end;

                suppose

                 A10: u <> i;

                (g . u) = ( IFEQ (i,u,e,(f . u))) by A6, A9

                .= (f . u) by A10, FUNCOP_1:def 8;

                hence thesis by A2, A9;

              end;

            end;

            then g in Y by A3;

            hence e in (Y . i) by A4, A7;

          end;

          assume

           A11: e in (Y . i);

          g in Y

          proof

            let u be object such that

             A12: u in I;

            per cases ;

              suppose u = i;

              hence thesis by A7, A11;

            end;

              suppose

               A13: u <> i;

              f in X by A2;

              then

               A14: f in Y by A3;

              (g . u) = ( IFEQ (i,u,e,(f . u))) by A6, A12

              .= (f . u) by A13, FUNCOP_1:def 8;

              hence thesis by A12, A14;

            end;

          end;

          then g in X by A3;

          hence e in (X . i) by A4, A7;

        end;

        hence (X . i) = (Y . i) by TARSKI: 2;

      end;

      hence thesis;

    end;

    theorem :: PBOOLE:136

    (for x holds x in X iff x in Y & x in Z) implies X = (Y (/\) Z)

    proof

      assume

       A1: for x holds x in X iff x in Y & x in Z;

      now

        let x;

        hereby

          assume x in X;

          then x in Y & x in Z by A1;

          hence x in (Y (/\) Z) by Th8;

        end;

        assume x in (Y (/\) Z);

        then x in Y & x in Z by Th8;

        hence x in X by A1;

      end;

      hence thesis by Th135;

    end;

    begin

    scheme :: PBOOLE:sch3

    MSSEx { I() -> set , P[ object, object] } :

ex f be ManySortedSet of I() st for i be object st i in I() holds P[i, (f . i)]

      provided

       A1: for i be object st i in I() holds ex j be object st P[i, j];

      consider f be Function such that

       A2: ( dom f) = I() and

       A3: for i be object st i in I() holds P[i, (f . i)] from CLASSES1:sch 1( A1);

      reconsider f as ManySortedSet of I() by A2, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      thus thesis by A3;

    end;

    scheme :: PBOOLE:sch4

    MSSLambda { I() -> set , F( object) -> object } :

ex f be ManySortedSet of I() st for i be object st i in I() holds (f . i) = F(i);

      consider f be Function such that

       A1: ( dom f) = I() and

       A2: for i be object st i in I() holds (f . i) = F(i) from FUNCT_1:sch 3;

      reconsider f as ManySortedSet of I() by A1, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      thus thesis by A2;

    end;

    registration

      let I be set;

      cluster Function-yielding for ManySortedSet of I;

      existence

      proof

        set f = the Function;

        reconsider F = (I --> f) as ManySortedSet of I;

        take F;

        let x be object;

        assume x in ( dom F);

        thus thesis;

      end;

    end

    definition

      let I be set;

      mode ManySortedFunction of I is Function-yielding ManySortedSet of I;

    end

    theorem :: PBOOLE:137

     not ex M be non-empty ManySortedSet of I st {} in ( rng M)

    proof

      let M be non-empty ManySortedSet of I;

      

       A1: ( dom M) = I by PARTFUN1:def 2;

      assume {} in ( rng M);

      then ex i be object st i in I & (M . i) = {} by A1, FUNCT_1:def 3;

      hence contradiction by Def13;

    end;

    definition

      let M be Function;

      mode Component of M is Element of ( rng M);

    end

    theorem :: PBOOLE:138

    for I be non empty set holds for M be ManySortedSet of I, A be Component of M holds ex i be object st i in I & A = (M . i)

    proof

      let I be non empty set;

      let M be ManySortedSet of I, A be Component of M;

      

       A1: ( dom M) = I by PARTFUN1:def 2;

      then ( rng M) <> {} by RELAT_1: 42;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    theorem :: PBOOLE:139

    for M be ManySortedSet of I, i st i in I holds (M . i) is Component of M

    proof

      let M be ManySortedSet of I, i;

      assume

       A1: i in I;

      ( dom M) = I by PARTFUN1:def 2;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    definition

      let I;

      let B be ManySortedSet of I;

      :: PBOOLE:def14

      mode Element of B -> ManySortedSet of I means for i be object st i in I holds (it . i) is Element of (B . i);

      existence

      proof

        defpred Q[ object, object] means $2 is Element of (B . $1);

        

         A1: for i be object st i in I holds ex j be object st Q[i, j]

        proof

          let i be object such that i in I;

          set j = the Element of (B . i);

          reconsider j as set;

          take j;

          thus thesis;

        end;

        thus ex f be ManySortedSet of I st for i be object st i in I holds Q[i, (f . i)] from MSSEx( A1);

      end;

    end

    begin

    definition

      let I;

      let A be ManySortedSet of I, B be ManySortedSet of I;

      :: PBOOLE:def15

      mode ManySortedFunction of A,B -> ManySortedSet of I means

      : Def15: for i st i in I holds (it . i) is Function of (A . i), (B . i);

      correctness

      proof

        defpred P[ object, object] means $2 is Function of (A . $1), (B . $1);

        

         A1: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object such that i in I;

          set j = the Function of (A . i), (B . i);

          reconsider j as set;

          take j;

          thus thesis;

        end;

        consider f be ManySortedSet of I such that

         A2: for i be object st i in I holds P[i, (f . i)] from MSSEx( A1);

        f is Function-yielding

        proof

          let i be object;

          assume i in ( dom f);

          then i in I by PARTFUN1:def 2;

          hence thesis by A2;

        end;

        then

        reconsider f as ManySortedFunction of I;

        take f;

        let i;

        assume i in I;

        hence thesis by A2;

      end;

    end

    registration

      let I;

      let A be ManySortedSet of I, B be ManySortedSet of I;

      cluster -> Function-yielding for ManySortedFunction of A, B;

      coherence

      proof

        let f be ManySortedFunction of A, B;

        let i be object;

        assume i in ( dom f);

        then i in I by PARTFUN1:def 2;

        hence thesis by Def15;

      end;

    end

    registration

      let I be set;

      let J be non empty set;

      let O be Function of I, J;

      let F be ManySortedSet of J;

      cluster (F * O) -> total;

      coherence

      proof

        

         A1: ( dom F) = J by PARTFUN1:def 2;

        ( rng O) c= J & ( dom O) = I by FUNCT_2:def 1, RELAT_1:def 19;

        then ( dom (F * O)) = I by A1, RELAT_1: 27;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    reserve D for non empty set,

n for Nat;

    scheme :: PBOOLE:sch5

    LambdaDMS { D() -> non empty set , F( object) -> object } :

ex X be ManySortedSet of D() st for d be Element of D() holds (X . d) = F(d);

      consider f be Function such that

       A1: ( dom f) = D() and

       A2: for d be Element of D() holds (f . d) = F(d) from FUNCT_1:sch 4;

      f is ManySortedSet of D() by A1, PARTFUN1:def 2, RELAT_1:def 18;

      hence thesis by A2;

    end;

    registration

      let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J;

      cluster (B . j) -> non empty;

      coherence by Def13;

    end

    reserve X,Y for ManySortedSet of I;

    definition

      let I, X, Y;

      :: PBOOLE:def16

      func [|X,Y|] -> ManySortedSet of I means for i be object st i in I holds (it . i) = [:(X . i), (Y . i):];

      existence

      proof

        deffunc F( object) = [:(X . $1), (Y . $1):];

        consider f be Function such that

         A1: ( dom f) = I & for i be object st i in I holds (f . i) = F(i) from FUNCT_1:sch 3;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of I;

        assume that

         A2: for i be object st i in I holds (f . i) = [:(X . i), (Y . i):] and

         A3: for i be object st i in I holds (g . i) = [:(X . i), (Y . i):];

        for x be object st x in I holds (f . x) = (g . x)

        proof

          let x be object;

          assume

           A4: x in I;

          then (f . x) = [:(X . x), (Y . x):] by A2;

          hence thesis by A3, A4;

        end;

        hence thesis;

      end;

    end

    definition

      let I, X, Y;

      deffunc F( object) = ( Funcs ((X . $1),(Y . $1)));

      :: PBOOLE:def17

      func (Funcs) (X,Y) -> ManySortedSet of I means for i be object st i in I holds (it . i) = ( Funcs ((X . i),(Y . i)));

      existence

      proof

        thus ex M be ManySortedSet of I st for i be object st i in I holds (M . i) = F(i) from MSSLambda;

      end;

      uniqueness

      proof

        let F1,F2 be ManySortedSet of I such that

         A1: for i be object st i in I holds (F1 . i) = ( Funcs ((X . i),(Y . i))) and

         A2: for i be object st i in I holds (F2 . i) = ( Funcs ((X . i),(Y . i)));

        now

          let i be object;

          assume

           A3: i in I;

          

          hence (F1 . i) = ( Funcs ((X . i),(Y . i))) by A1

          .= (F2 . i) by A2, A3;

        end;

        hence thesis;

      end;

    end

    definition

      let I be set, M be ManySortedSet of I;

      :: PBOOLE:def18

      mode ManySortedSubset of M -> ManySortedSet of I means

      : Def18: it c= M;

      existence ;

    end

    registration

      let I be set, M be non-empty ManySortedSet of I;

      cluster non-empty for ManySortedSubset of M;

      existence

      proof

        reconsider N = M as ManySortedSubset of M by Def18;

        take N;

        thus thesis;

      end;

    end

    definition

      let F,G be Function-yielding Function;

      :: PBOOLE:def19

      func G ** F -> Function means

      : Def19: ( dom it ) = (( dom F) /\ ( dom G)) & for i be object st i in ( dom it ) holds (it . i) = ((G . i) * (F . i));

      existence

      proof

        defpred P[ object, object] means $2 = ((G . $1) * (F . $1));

        

         A1: for i be object st i in (( dom F) /\ ( dom G)) holds ex u be object st P[i, u];

        ex H be Function st ( dom H) = (( dom F) /\ ( dom G)) & for i be object st i in (( dom F) /\ ( dom G)) holds P[i, (H . i)] from CLASSES1:sch 1( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let H1,H2 be Function;

        assume that

         A2: ( dom H1) = (( dom F) /\ ( dom G)) and

         A3: for i be object st i in ( dom H1) holds (H1 . i) = ((G . i) * (F . i)) and

         A4: ( dom H2) = (( dom F) /\ ( dom G)) and

         A5: for i be object st i in ( dom H2) holds (H2 . i) = ((G . i) * (F . i));

        now

          let i be object;

          reconsider f = (F . i) as Function;

          reconsider g = (G . i) as Function;

          assume

           A6: i in (( dom F) /\ ( dom G));

          then (H1 . i) = (g * f) by A2, A3;

          hence (H1 . i) = (H2 . i) by A4, A5, A6;

        end;

        hence thesis by A2, A4;

      end;

    end

    registration

      let F,G be Function-yielding Function;

      cluster (G ** F) -> Function-yielding;

      coherence

      proof

        set H = (G ** F);

        let x be object;

        reconsider f = (F . x) as Function;

        reconsider g = (G . x) as Function;

        assume x in ( dom H);

        then (H . x) = (g * f) by Def19;

        hence thesis;

      end;

    end

    definition

      let I be set, A be ManySortedSet of I, F be ManySortedFunction of I;

      :: PBOOLE:def20

      func F .:.: A -> ManySortedSet of I means for i be set st i in I holds (it . i) = ((F . i) .: (A . i));

      existence

      proof

        defpred P[ object, object] means $2 = ((F . $1) .: (A . $1));

        

         A1: for i be object st i in I holds ex u be object st P[i, u];

        consider g be Function such that

         A2: ( dom g) = I & for i be object st i in I holds P[i, (g . i)] from CLASSES1:sch 1( A1);

        reconsider g as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;

        take g;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let B,B1 be ManySortedSet of I;

        assume that

         A3: for i be set st i in I holds (B . i) = ((F . i) .: (A . i)) and

         A4: for i be set st i in I holds (B1 . i) = ((F . i) .: (A . i));

        now

          let i be object;

          reconsider f = (F . i) as Function;

          assume

           A5: i in I;

          then (B . i) = (f .: (A . i)) by A3;

          hence (B . i) = (B1 . i) by A4, A5;

        end;

        hence thesis;

      end;

    end

    registration

      let I;

      cluster ( EmptyMS I) -> empty-yielding;

      coherence ;

    end

    scheme :: PBOOLE:sch6

    MSSExD { I() -> non empty set , P[ object, object] } :

ex f be ManySortedSet of I() st for i be Element of I() holds P[i, (f . i)]

      provided

       A1: for i be Element of I() holds ex j be object st P[i, j];

      

       A2: for i be object st i in I() holds ex j be object st P[i, j] by A1;

      consider f be ManySortedSet of I() such that

       A3: for i be object st i in I() holds P[i, (f . i)] from MSSEx( A2);

      take f;

      let i be Element of I();

      thus thesis by A3;

    end;

    registration

      let A be non empty set;

      cluster non-empty -> non empty-yielding for ManySortedSet of A;

      coherence ;

    end

    registration

      let X be non empty set;

      cluster -> non empty for ManySortedSet of X;

      coherence ;

    end

    theorem :: PBOOLE:140

    for F,G,H be Function-yielding Function holds ((H ** G) ** F) = (H ** (G ** F))

    proof

      let F,G,H be Function-yielding Function;

      set f = ((H ** G) ** F), g = (H ** (G ** F));

      now

        

         A1: ( dom f) = (( dom (H ** G)) /\ ( dom F)) by Def19

        .= ((( dom H) /\ ( dom G)) /\ ( dom F)) by Def19;

        then

         A2: ( dom f) = (( dom H) /\ (( dom G) /\ ( dom F))) by XBOOLE_1: 16;

        

        hence

         A3: ( dom f) = (( dom H) /\ ( dom (G ** F))) by Def19

        .= ( dom g) by Def19;

        let x be object;

        assume

         A4: x in ( dom f);

        then x in (( dom H) /\ ( dom G)) by A1, XBOOLE_0:def 4;

        then

         A5: x in ( dom (H ** G)) by Def19;

        x in (( dom G) /\ ( dom F)) by A2, A4, XBOOLE_0:def 4;

        then

         A6: x in ( dom (G ** F)) by Def19;

        

        thus (f . x) = (((H ** G) . x) * (F . x)) by A4, Def19

        .= (((H . x) * (G . x)) * (F . x)) by A5, Def19

        .= ((H . x) * ((G . x) * (F . x))) by RELAT_1: 36

        .= ((H . x) * ((G ** F) . x)) by A6, Def19

        .= (g . x) by A3, A4, Def19;

      end;

      hence thesis;

    end;

    registration

      let I be set, f be non-empty ManySortedSet of I;

      cluster total for I -definedf -compatible Function;

      existence

      proof

        deffunc F( object) = (f . $1);

        

         A1: for e be object st e in I holds F(e) <> {} ;

        consider g be ManySortedSet of I such that

         A2: for e be object st e in I holds (g . e) in F(e) from KuratowskiFunction( A1);

        g is f -compatible

        proof

          let x be object;

          assume x in ( dom g);

          then x in I by PARTFUN1:def 2;

          hence (g . x) in (f . x) by A2;

        end;

        then

        reconsider g as I -definedf -compatible Function;

        take g;

        thus g is total;

      end;

    end

    theorem :: PBOOLE:141

    for I be set, f be non-empty ManySortedSet of I holds for p be f -compatibleI -defined Function holds ex s be f -compatible ManySortedSet of I st p c= s

    proof

      let I be set, f be non-empty ManySortedSet of I;

      let p be f -compatibleI -defined Function;

      set h = the f -compatible ManySortedSet of I;

      take (h +* p);

      thus p c= (h +* p) by FUNCT_4: 25;

    end;

    theorem :: PBOOLE:142

    for I,A be set holds for s,ss be ManySortedSet of I holds ((ss +* (s | A)) | A) = (s | A)

    proof

      let I,A be set;

      let s,ss be ManySortedSet of I;

      ( dom s) = I by PARTFUN1:def 2

      .= ( dom ss) by PARTFUN1:def 2;

      then (A /\ ( dom ss)) c= (A /\ ( dom s));

      hence thesis by FUNCT_4: 88;

    end;

    registration

      let X be non empty set, Y be set;

      cluster X -valued for ManySortedSet of Y;

      existence

      proof

        take M = (Y --> the Element of X);

        

         A1: { the Element of X} c= X by ZFMISC_1: 31;

        ( rng M) c= { the Element of X} by FUNCOP_1: 13;

        hence ( rng M) c= X by A1;

      end;

    end

    theorem :: PBOOLE:143

    for I,Y be non empty set, M be Y -valued ManySortedSet of I, x be Element of I holds (M . x) = (M /. x)

    proof

      let I,Y be non empty set, M be Y -valued ManySortedSet of I, x be Element of I;

      ( dom M) = I by PARTFUN1:def 2;

      hence (M . x) = (M /. x) by PARTFUN1:def 6;

    end;

    theorem :: PBOOLE:144

    for f be Function, M be ManySortedSet of I holds ((f +* M) | I) = M

    proof

      let f be Function, M be ManySortedSet of I;

      

       A1: ( dom (f | I)) c= I by RELAT_1: 58;

      

       A2: ( dom M) = I by PARTFUN1:def 2;

      

      thus ((f +* M) | I) = ((f | I) +* (M | I)) by FUNCT_4: 71

      .= ((f | I) +* M)

      .= M by A1, A2, FUNCT_4: 19;

    end;

    theorem :: PBOOLE:145

    for I be set, Y be non empty set holds for p be Y -valuedI -defined Function holds ex s be Y -valued ManySortedSet of I st p c= s

    proof

      let I be set, Y be non empty set;

      let p be Y -valuedI -defined Function;

      set h = the Y -valued ManySortedSet of I;

      take (h +* p);

      thus p c= (h +* p) by FUNCT_4: 25;

    end;

    theorem :: PBOOLE:146

    X c= Y & Y c= X implies X = Y by Lm1;

    definition

      let I be non empty set, A,B be ManySortedSet of I;

      :: original: =

      redefine

      :: PBOOLE:def21

      pred A = B means for i be Element of I holds (A . i) = (B . i);

      compatibility ;

    end

    registration

      let X be with_non-empty_elements set;

      cluster ( id X) -> non-empty;

      coherence by SETFAM_1:def 8;

    end

    scheme :: PBOOLE:sch7

    MSSLambda { I() -> set , F( object) -> object } :

ex f be ManySortedSet of I() st for i be set st i in I() holds (f . i) = F(i);

      consider f be Function such that

       A1: ( dom f) = I() and

       A2: for i be object st i in I() holds (f . i) = F(i) from FUNCT_1:sch 3;

      reconsider f as ManySortedSet of I() by A1, PARTFUN1:def 2, RELAT_1:def 18;

      take f;

      thus thesis by A2;

    end;