mboolean.miz



    begin

    reserve x,y for object,

I for set,

A,B,X,Y for ManySortedSet of I;

    definition

      let I, A;

      :: MBOOLEAN:def1

      func bool A -> ManySortedSet of I means

      : Def1: for i be object st i in I holds (it . i) = ( bool (A . i));

      existence

      proof

        deffunc V( object) = ( bool (A . $1));

        thus ex X be ManySortedSet of I st for i be object st i in I holds (X . i) = V(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) = ( bool (A . i)) and

         A2: for i be object st i in I holds (Y . i) = ( bool (A . i));

        now

          let i be object;

          assume

           A3: i in I;

          

          hence (X . i) = ( bool (A . i)) by A1

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

        end;

        hence X = Y;

      end;

    end

    registration

      let I, A;

      cluster ( bool A) -> non-empty;

      coherence

      proof

        let i be object such that

         A1: i in I;

        ( bool (A . i)) is non empty;

        hence thesis by A1, Def1;

      end;

    end

    

     Lm1: for i,I,X be set holds for M be ManySortedSet of I st i in I holds ( dom (M +* (i .--> X))) = I

    proof

      let i,I,X be set, 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;

    

     Lm2: for i be set st i in I holds (( bool (A (\/) B)) . i) = ( bool ((A . i) \/ (B . i)))

    proof

      let i be set;

      assume

       A1: i in I;

      

      hence (( bool (A (\/) B)) . i) = ( bool ((A (\/) B) . i)) by Def1

      .= ( bool ((A . i) \/ (B . i))) by A1, PBOOLE:def 4;

    end;

    

     Lm3: for i be set st i in I holds (( bool (A (/\) B)) . i) = ( bool ((A . i) /\ (B . i)))

    proof

      let i be set;

      assume

       A1: i in I;

      

      hence (( bool (A (/\) B)) . i) = ( bool ((A (/\) B) . i)) by Def1

      .= ( bool ((A . i) /\ (B . i))) by A1, PBOOLE:def 5;

    end;

    

     Lm4: for i be set st i in I holds (( bool (A (\) B)) . i) = ( bool ((A . i) \ (B . i)))

    proof

      let i be set;

      assume

       A1: i in I;

      

      hence (( bool (A (\) B)) . i) = ( bool ((A (\) B) . i)) by Def1

      .= ( bool ((A . i) \ (B . i))) by A1, PBOOLE:def 6;

    end;

    

     Lm5: for i be set st i in I holds (( bool (A (\+\) B)) . i) = ( bool ((A . i) \+\ (B . i)))

    proof

      let i be set;

      assume

       A1: i in I;

      

      hence (( bool (A (\+\) B)) . i) = ( bool ((A (\+\) B) . i)) by Def1

      .= ( bool ((A . i) \+\ (B . i))) by A1, PBOOLE: 4;

    end;

    theorem :: MBOOLEAN:1

    

     Th1: X = ( bool Y) iff for A holds A in X iff A c= Y

    proof

      thus X = ( bool Y) implies for A holds A in X iff A c= Y

      proof

        assume

         A1: X = ( bool Y);

        let A;

        thus A in X implies A c= Y

        proof

          assume

           A2: A in X;

          let i be object;

          assume

           A3: i in I;

          then

           A4: (A . i) in (X . i) by A2;

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

          hence thesis by A4;

        end;

        assume

         A5: A c= Y;

        let i be object;

        assume

         A6: i in I;

        then

         A7: (A . i) c= (Y . i) by A5;

        (X . i) = ( bool (Y . i)) by A1, A6, Def1;

        hence thesis by A7;

      end;

      assume

       A8: for A holds A in X iff A c= Y;

      now

        let i be object such that

         A9: i in I;

        ( EmptyMS I) c= Y by PBOOLE: 43;

        then

         A10: ( EmptyMS I) in X by A8;

        for A9 be set holds A9 in (X . i) iff A9 c= (Y . i)

        proof

          let A9 be set;

          

           A11: ( dom (i .--> A9)) = {i};

          ( dom (( EmptyMS I) +* (i .--> A9))) = I by A9, Lm1;

          then

          reconsider K = (( EmptyMS I) +* (i .--> A9)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

          i in {i} by TARSKI:def 1;

          

          then

           A12: (K . i) = ((i .--> A9) . i) by A11, FUNCT_4: 13

          .= A9 by FUNCOP_1: 72;

          thus A9 in (X . i) implies A9 c= (Y . i)

          proof

            assume

             A13: A9 in (X . i);

            K in X

            proof

              let j be object such that

               A14: j in I;

              now

                per cases ;

                  case j = i;

                  hence thesis by A12, A13;

                end;

                  case j <> i;

                  then not j in ( dom (i .--> A9)) by TARSKI:def 1;

                  then (K . j) = (( EmptyMS I) . j) by FUNCT_4: 11;

                  hence thesis by A10, A14;

                end;

              end;

              hence thesis;

            end;

            then K c= Y by A8;

            hence thesis by A9, A12;

          end;

          assume

           A15: A9 c= (Y . i);

          K c= Y

          proof

            let j be object such that

             A16: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A12, A15;

              end;

                case j <> i;

                then not j in ( dom (i .--> A9)) by TARSKI:def 1;

                then

                 A17: (K . j) = (( EmptyMS I) . j) by FUNCT_4: 11;

                ( EmptyMS I) c= Y by PBOOLE: 43;

                hence thesis by A16, A17;

              end;

            end;

            hence thesis;

          end;

          then K in X by A8;

          hence thesis by A9, A12;

        end;

        then (X . i) = ( bool (Y . i)) by ZFMISC_1:def 1;

        hence (X . i) = (( bool Y) . i) by A9, Def1;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:2

    ( bool ( EmptyMS I)) = (I --> { {} })

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        then (( bool ( EmptyMS I)) . i) = ( bool (( EmptyMS I) . i)) by Def1

        .= ( bool {} ) by PBOOLE: 5

        .= { {} } by ZFMISC_1: 1;

        hence (( bool ( EmptyMS I)) . i) = ((I --> { {} }) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:3

    for x be set holds ( bool (I --> x)) = (I --> ( bool x))

    proof

      let x be set;

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( bool (I --> x)) . i) = ( bool ((I --> x) . i)) by Def1

        .= ( bool x) by A1, FUNCOP_1: 7

        .= ((I --> ( bool x)) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:4

    ( bool (I --> {x})) = (I --> { {} , {x}})

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( bool (I --> {x})) . i) = ( bool ((I --> {x}) . i)) by Def1

        .= ( bool {x}) by A1, FUNCOP_1: 7

        .= { {} , {x}} by ZFMISC_1: 24

        .= ((I --> { {} , {x}}) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:5

    ( EmptyMS I) c= A

    proof

      let i be object;

      assume i in I;

      (( EmptyMS I) . i) = {} by PBOOLE: 5;

      hence thesis by XBOOLE_1: 2;

    end;

    theorem :: MBOOLEAN:6

    A c= B implies ( bool A) c= ( bool B)

    proof

      assume

       A1: A c= B;

      let i be object;

      assume

       A2: i in I;

      then

       A3: (A . i) c= (B . i) by A1;

      (( bool A) . i) = ( bool (A . i)) & (( bool B) . i) = ( bool (B . i)) by A2, Def1;

      hence thesis by A3, ZFMISC_1: 67;

    end;

    theorem :: MBOOLEAN:7

    (( bool A) (\/) ( bool B)) c= ( bool (A (\/) B))

    proof

      let i be object;

      assume

       A1: i in I;

      then

       A2: (( bool (A (\/) B)) . i) = ( bool ((A . i) \/ (B . i))) by Lm2;

      ((( bool A) (\/) ( bool B)) . i) = ((( bool A) . i) \/ (( bool B) . i)) by A1, PBOOLE:def 4

      .= (( bool (A . i)) \/ (( bool B) . i)) by A1, Def1

      .= (( bool (A . i)) \/ ( bool (B . i))) by A1, Def1;

      hence thesis by A2, ZFMISC_1: 69;

    end;

    theorem :: MBOOLEAN:8

    (( bool A) (\/) ( bool B)) = ( bool (A (\/) B)) implies for i be set st i in I holds ((A . i),(B . i)) are_c=-comparable

    proof

      assume

       A1: (( bool A) (\/) ( bool B)) = ( bool (A (\/) B));

      let i be set such that

       A2: i in I;

      ( bool ((A . i) \/ (B . i))) = ((( bool A) (\/) ( bool B)) . i) by A1, A2, Lm2

      .= ((( bool A) . i) \/ (( bool B) . i)) by A2, PBOOLE:def 4

      .= ((( bool A) . i) \/ ( bool (B . i))) by A2, Def1

      .= (( bool (A . i)) \/ ( bool (B . i))) by A2, Def1;

      hence thesis by ZFMISC_1: 70;

    end;

    theorem :: MBOOLEAN:9

    ( bool (A (/\) B)) = (( bool A) (/\) ( bool B))

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( bool (A (/\) B)) . i) = ( bool ((A . i) /\ (B . i))) by Lm3

        .= (( bool (A . i)) /\ ( bool (B . i))) by ZFMISC_1: 71

        .= (( bool (A . i)) /\ (( bool B) . i)) by A1, Def1

        .= ((( bool A) . i) /\ (( bool B) . i)) by A1, Def1

        .= ((( bool A) (/\) ( bool B)) . i) by A1, PBOOLE:def 5;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:10

    ( bool (A (\) B)) c= ((I --> { {} }) (\/) (( bool A) (\) ( bool B)))

    proof

      let i be object;

      assume

       A1: i in I;

      then

       A2: (( bool (A (\) B)) . i) = ( bool ((A . i) \ (B . i))) by Lm4;

      (((I --> { {} }) (\/) (( bool A) (\) ( bool B))) . i) = (((I --> { {} }) . i) \/ ((( bool A) (\) ( bool B)) . i)) by A1, PBOOLE:def 4

      .= ( { {} } \/ ((( bool A) (\) ( bool B)) . i)) by A1, FUNCOP_1: 7

      .= ( { {} } \/ ((( bool A) . i) \ (( bool B) . i))) by A1, PBOOLE:def 6

      .= ( { {} } \/ (( bool (A . i)) \ (( bool B) . i))) by A1, Def1

      .= ( { {} } \/ (( bool (A . i)) \ ( bool (B . i)))) by A1, Def1;

      hence thesis by A2, ZFMISC_1: 72;

    end;

    theorem :: MBOOLEAN:11

    X c= (A (\) B) iff X c= A & X misses B

    proof

      thus X c= (A (\) B) implies X c= A & X misses B

      proof

        assume X c= (A (\) B);

        then

         A1: X in ( bool (A (\) B)) by Th1;

        thus X c= A

        proof

          let i be object;

          assume

           A2: i in I;

          then (X . i) in (( bool (A (\) B)) . i) by A1;

          then (X . i) in ( bool ((A . i) \ (B . i))) by A2, Lm4;

          hence thesis by XBOOLE_1: 106;

        end;

        let i be object;

        assume

         A3: i in I;

        then (X . i) in (( bool (A (\) B)) . i) by A1;

        then (X . i) in ( bool ((A . i) \ (B . i))) by A3, Lm4;

        hence thesis by XBOOLE_1: 106;

      end;

      assume

       A4: X c= A & X misses B;

      let i be object;

      assume

       A5: i in I;

      then (X . i) c= (A . i) & (X . i) misses (B . i) by A4;

      then (X . i) c= ((A . i) \ (B . i)) by XBOOLE_1: 86;

      hence thesis by A5, PBOOLE:def 6;

    end;

    theorem :: MBOOLEAN:12

    (( bool (A (\) B)) (\/) ( bool (B (\) A))) c= ( bool (A (\+\) B))

    proof

      let i be object;

      assume

       A1: i in I;

      then

       A2: (( bool (A (\+\) B)) . i) = ( bool ((A . i) \+\ (B . i))) by Lm5;

      ((( bool (A (\) B)) (\/) ( bool (B (\) A))) . i) = ((( bool (A (\) B)) . i) \/ (( bool (B (\) A)) . i)) by A1, PBOOLE:def 4

      .= (( bool ((A . i) \ (B . i))) \/ (( bool (B (\) A)) . i)) by A1, Lm4

      .= (( bool ((A . i) \ (B . i))) \/ ( bool ((B . i) \ (A . i)))) by A1, Lm4;

      hence thesis by A2, ZFMISC_1: 73;

    end;

    theorem :: MBOOLEAN:13

    X c= (A (\+\) B) iff X c= (A (\/) B) & X misses (A (/\) B)

    proof

      thus X c= (A (\+\) B) implies X c= (A (\/) B) & X misses (A (/\) B)

      proof

        assume X c= (A (\+\) B);

        then

         A1: X in ( bool (A (\+\) B)) by Th1;

        thus X c= (A (\/) B)

        proof

          let i be object;

          assume

           A2: i in I;

          then (X . i) in (( bool (A (\+\) B)) . i) by A1;

          then (X . i) in ( bool ((A . i) \+\ (B . i))) by A2, Lm5;

          then (X . i) c= ((A . i) \/ (B . i)) by XBOOLE_1: 107;

          hence thesis by A2, PBOOLE:def 4;

        end;

        let i be object;

        assume

         A3: i in I;

        then (X . i) in (( bool (A (\+\) B)) . i) by A1;

        then (X . i) in ( bool ((A . i) \+\ (B . i))) by A3, Lm5;

        then (X . i) misses ((A . i) /\ (B . i)) by XBOOLE_1: 107;

        hence thesis by A3, PBOOLE:def 5;

      end;

      assume that

       A4: X c= (A (\/) B) and

       A5: X misses (A (/\) B);

      let i be object;

      assume

       A6: i in I;

      then (X . i) misses ((A (/\) B) . i) by A5;

      then

       A7: (X . i) misses ((A . i) /\ (B . i)) by A6, PBOOLE:def 5;

      (X . i) c= ((A (\/) B) . i) by A4, A6;

      then (X . i) c= ((A . i) \/ (B . i)) by A6, PBOOLE:def 4;

      then (X . i) c= ((A . i) \+\ (B . i)) by A7, XBOOLE_1: 107;

      hence thesis by A6, PBOOLE: 4;

    end;

    theorem :: MBOOLEAN:14

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

    proof

      assume

       A1: X c= A or Y c= A;

      per cases by A1;

        suppose

         A2: X c= A;

        let i be object;

        assume

         A3: i in I;

        then (X . i) c= (A . i) by A2;

        then ((X . i) /\ (Y . i)) c= (A . i) by XBOOLE_1: 108;

        hence thesis by A3, PBOOLE:def 5;

      end;

        suppose

         A4: Y c= A;

        let i be object;

        assume

         A5: i in I;

        then (Y . i) c= (A . i) by A4;

        then ((X . i) /\ (Y . i)) c= (A . i) by XBOOLE_1: 108;

        hence thesis by A5, PBOOLE:def 5;

      end;

    end;

    theorem :: MBOOLEAN:15

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

    proof

      assume

       A1: X c= A;

      let i be object;

      assume

       A2: i in I;

      then (X . i) c= (A . i) by A1;

      then ((X . i) \ (Y . i)) c= (A . i) by XBOOLE_1: 109;

      hence thesis by A2, PBOOLE:def 6;

    end;

    theorem :: MBOOLEAN:16

    X c= A & Y c= A implies (X (\+\) Y) c= A

    proof

      assume

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

      let i be object;

      assume

       A2: i in I;

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

      then ((X . i) \+\ (Y . i)) c= (A . i) by XBOOLE_1: 110;

      then ((X . i) \+\ (Y . i)) in ( bool (A . i));

      then ((X (\+\) Y) . i) in ( bool (A . i)) by A2, PBOOLE: 4;

      hence thesis;

    end;

    theorem :: MBOOLEAN:17

     [|X, Y|] c= ( bool ( bool (X (\/) Y)))

    proof

      let i be object;

      assume

       A1: i in I;

      then

       A2: ( [|X, Y|] . i) = [:(X . i), (Y . i):] by PBOOLE:def 16;

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

      .= ( bool ( bool ((X . i) \/ (Y . i)))) by A1, Lm2;

      hence thesis by A2, ZFMISC_1: 86;

    end;

    theorem :: MBOOLEAN:18

    X c= A iff X in ( bool A)

    proof

      thus X c= A implies X in ( bool A)

      proof

        assume

         A1: X c= A;

        let i be object;

        assume

         A2: i in I;

        then (X . i) c= (A . i) by A1;

        then (X . i) in ( bool (A . i));

        hence thesis by A2, Def1;

      end;

      assume

       A3: X in ( bool A);

      let i be object;

      assume

       A4: i in I;

      then (X . i) in (( bool A) . i) by A3;

      then (X . i) in ( bool (A . i)) by A4, Def1;

      hence thesis;

    end;

    theorem :: MBOOLEAN:19

    ( (Funcs) (A,B)) c= ( bool [|A, B|])

    proof

      let i be object;

      assume

       A1: i in I;

      then

       A2: (( (Funcs) (A,B)) . i) = ( Funcs ((A . i),(B . i))) by PBOOLE:def 17;

      (( bool [|A, B|]) . i) = ( bool ( [|A, B|] . i)) by A1, Def1

      .= ( bool [:(A . i), (B . i):]) by A1, PBOOLE:def 16;

      hence thesis by A2, FRAENKEL: 2;

    end;

    begin

    definition

      let I, A;

      :: MBOOLEAN:def2

      func union A -> ManySortedSet of I means

      : Def2: for i be object st i in I holds (it . i) = ( union (A . i));

      existence

      proof

        deffunc V( object) = ( union (A . $1));

        thus ex X be ManySortedSet of I st for i be object st i in I holds (X . i) = V(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) = ( union (A . i)) and

         A2: for i be object st i in I holds (Y . i) = ( union (A . i));

        now

          let i be object;

          assume

           A3: i in I;

          

          hence (X . i) = ( union (A . i)) by A1

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

        end;

        hence X = Y;

      end;

    end

    registration

      let I;

      cluster ( union ( EmptyMS I)) -> empty-yielding;

      coherence

      proof

        let i be object;

        

         A1: ( union (( EmptyMS I) . i)) is empty by PBOOLE: 5, ZFMISC_1: 2;

        assume i in I;

        hence thesis by A1, Def2;

      end;

    end

    

     Lm6: for i be set st i in I holds (( union (A (\/) B)) . i) = ( union ((A . i) \/ (B . i)))

    proof

      let i be set;

      assume

       A1: i in I;

      

      hence (( union (A (\/) B)) . i) = ( union ((A (\/) B) . i)) by Def2

      .= ( union ((A . i) \/ (B . i))) by A1, PBOOLE:def 4;

    end;

    

     Lm7: for i be set st i in I holds (( union (A (/\) B)) . i) = ( union ((A . i) /\ (B . i)))

    proof

      let i be set;

      assume

       A1: i in I;

      

      hence (( union (A (/\) B)) . i) = ( union ((A (/\) B) . i)) by Def2

      .= ( union ((A . i) /\ (B . i))) by A1, PBOOLE:def 5;

    end;

    theorem :: MBOOLEAN:20

    A in ( union X) iff ex Y st A in Y & Y in X

    proof

      thus A in ( union X) implies ex Y st A in Y & Y in X

      proof

        defpred P[ object, object] means ex B be set st B = $2 & (A . $1) in B & $2 in (X . $1);

        assume

         A1: A in ( union X);

        

         A2: for i be object st i in I holds ex Y be object st P[i, Y]

        proof

          let i be object;

          assume

           A3: i in I;

          then (A . i) in (( union X) . i) by A1;

          then (A . i) in ( union (X . i)) by A3, Def2;

          then

          consider B be set such that

           A4: (A . i) in B & B in (X . i) by TARSKI:def 4;

          take B;

          thus thesis by A4;

        end;

        consider K be ManySortedSet of I such that

         A5: for i be object st i in I holds P[i, (K . i)] from PBOOLE:sch 3( A2);

        take K;

        thus A in K

        proof

          let i be object;

          assume i in I;

          then P[i, (K . i)] by A5;

          hence thesis;

        end;

        thus K in X

        proof

          let i be object;

          assume i in I;

          then P[i, (K . i)] by A5;

          hence thesis;

        end;

      end;

      given Y such that

       A6: A in Y & Y in X;

      let i be object;

      assume

       A7: i in I;

      then (A . i) in (Y . i) & (Y . i) in (X . i) by A6;

      then (A . i) in ( union (X . i)) by TARSKI:def 4;

      hence thesis by A7, Def2;

    end;

    theorem :: MBOOLEAN:21

    ( union ( EmptyMS I)) = ( EmptyMS I)

    proof

      now

        let i be object;

        assume i in I;

        

        hence (( union ( EmptyMS I)) . i) = ( union (( EmptyMS I) . i)) by Def2

        .= {} by PBOOLE: 5, ZFMISC_1: 2

        .= (( EmptyMS I) . i) by PBOOLE: 5;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:22

    for x be set holds ( union (I --> x)) = (I --> ( union x))

    proof

      let x be set;

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( union (I --> x)) . i) = ( union ((I --> x) . i)) by Def2

        .= ( union x) by A1, FUNCOP_1: 7

        .= ((I --> ( union x)) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:23

    ( union (I --> {x})) = (I --> x)

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( union (I --> {x})) . i) = ( union ((I --> {x}) . i)) by Def2

        .= ( union {x}) by A1, FUNCOP_1: 7

        .= x by ZFMISC_1: 25

        .= ((I --> x) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:24

    ( union (I --> { {x}, {y}})) = (I --> {x, y})

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( union (I --> { {x}, {y}})) . i) = ( union ((I --> { {x}, {y}}) . i)) by Def2

        .= ( union { {x}, {y}}) by A1, FUNCOP_1: 7

        .= {x, y} by ZFMISC_1: 26

        .= ((I --> {x, y}) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:25

    X in A implies X c= ( union A)

    proof

      assume

       A1: X in A;

      let i be object;

      assume

       A2: i in I;

      then (X . i) in (A . i) by A1;

      then (X . i) c= ( union (A . i)) by ZFMISC_1: 74;

      hence thesis by A2, Def2;

    end;

    theorem :: MBOOLEAN:26

    A c= B implies ( union A) c= ( union B)

    proof

      assume

       A1: A c= B;

      let i be object;

      assume

       A2: i in I;

      then (A . i) c= (B . i) by A1;

      then ( union (A . i)) c= ( union (B . i)) by ZFMISC_1: 77;

      then (( union A) . i) c= ( union (B . i)) by A2, Def2;

      hence thesis by A2, Def2;

    end;

    theorem :: MBOOLEAN:27

    ( union (A (\/) B)) = (( union A) (\/) ( union B))

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( union (A (\/) B)) . i) = ( union ((A . i) \/ (B . i))) by Lm6

        .= (( union (A . i)) \/ ( union (B . i))) by ZFMISC_1: 78

        .= ((( union A) . i) \/ ( union (B . i))) by A1, Def2

        .= ((( union A) . i) \/ (( union B) . i)) by A1, Def2

        .= ((( union A) (\/) ( union B)) . i) by A1, PBOOLE:def 4;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:28

    ( union (A (/\) B)) c= (( union A) (/\) ( union B))

    proof

      let i be object;

      assume

       A1: i in I;

      then

       A2: (( union (A (/\) B)) . i) = ( union ((A . i) /\ (B . i))) by Lm7;

      ((( union A) (/\) ( union B)) . i) = ((( union A) . i) /\ (( union B) . i)) by A1, PBOOLE:def 5

      .= (( union (A . i)) /\ (( union B) . i)) by A1, Def2

      .= (( union (A . i)) /\ ( union (B . i))) by A1, Def2;

      hence thesis by A2, ZFMISC_1: 79;

    end;

    theorem :: MBOOLEAN:29

    ( union ( bool A)) = A

    proof

      now

        let i be object;

        assume

         A1: i in I;

        

        hence (( union ( bool A)) . i) = ( union (( bool A) . i)) by Def2

        .= ( union ( bool (A . i))) by A1, Def1

        .= (A . i) by ZFMISC_1: 81;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:30

    A c= ( bool ( union A))

    proof

      let i be object;

      assume

       A1: i in I;

      

      then (( bool ( union A)) . i) = ( bool (( union A) . i)) by Def1

      .= ( bool ( union (A . i))) by A1, Def2;

      hence thesis by ZFMISC_1: 82;

    end;

    theorem :: MBOOLEAN:31

    ( union Y) c= A & X in Y implies X c= A

    proof

      assume that

       A1: ( union Y) c= A and

       A2: X in Y;

      let i be object;

      assume

       A3: i in I;

      then (( union Y) . i) c= (A . i) by A1;

      then

       A4: ( union (Y . i)) c= (A . i) by A3, Def2;

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

      hence thesis by A4, SETFAM_1: 41;

    end;

    theorem :: MBOOLEAN:32

    for Z be ManySortedSet of I holds for A be non-empty ManySortedSet of I holds (for X be ManySortedSet of I st X in A holds X c= Z) implies ( union A) c= Z

    proof

      let Z be ManySortedSet of I, A be non-empty ManySortedSet of I;

      assume

       A1: for X be ManySortedSet of I st X in A holds X c= Z;

      let i be object such that

       A2: i in I;

      for X9 be set st X9 in (A . i) holds X9 c= (Z . i)

      proof

        consider M be ManySortedSet of I such that

         A3: M in A by PBOOLE: 134;

        let X9 be set such that

         A4: X9 in (A . i);

        ( dom (M +* (i .--> X9))) = I by A2, Lm1;

        then

        reconsider K = (M +* (i .--> X9)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        

         A5: ( dom (i .--> X9)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A6: (K . i) = ((i .--> X9) . i) by A5, FUNCT_4: 13

        .= X9 by FUNCOP_1: 72;

        K in A

        proof

          let j be object such that

           A7: j in I;

          now

            per cases ;

              case j = i;

              hence thesis by A4, A6;

            end;

              case j <> i;

              then not j in ( dom (i .--> X9)) by TARSKI:def 1;

              then (K . j) = (M . j) by FUNCT_4: 11;

              hence thesis by A3, A7;

            end;

          end;

          hence thesis;

        end;

        then K c= Z by A1;

        hence thesis by A2, A6;

      end;

      then ( union (A . i)) c= (Z . i) by ZFMISC_1: 76;

      hence thesis by A2, Def2;

    end;

    theorem :: MBOOLEAN:33

    for B be ManySortedSet of I holds for A be non-empty ManySortedSet of I st for X be ManySortedSet of I st X in A holds (X (/\) B) = ( EmptyMS I) holds (( union A) (/\) B) = ( EmptyMS I)

    proof

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

      assume

       A1: for X be ManySortedSet of I st X in A holds (X (/\) B) = ( EmptyMS I);

      now

        let i be object such that

         A2: i in I;

        for X9 be set st X9 in (A . i) holds X9 misses (B . i)

        proof

          consider M be ManySortedSet of I such that

           A3: M in A by PBOOLE: 134;

          let X9 be set such that

           A4: X9 in (A . i);

          ( dom (M +* (i .--> X9))) = I by A2, Lm1;

          then

          reconsider K = (M +* (i .--> X9)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

          

           A5: ( dom (i .--> X9)) = {i};

          i in {i} by TARSKI:def 1;

          

          then

           A6: (K . i) = ((i .--> X9) . i) by A5, FUNCT_4: 13

          .= X9 by FUNCOP_1: 72;

          K in A

          proof

            let j be object such that

             A7: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A4, A6;

              end;

                case j <> i;

                then not j in ( dom (i .--> X9)) by TARSKI:def 1;

                then (K . j) = (M . j) by FUNCT_4: 11;

                hence thesis by A3, A7;

              end;

            end;

            hence thesis;

          end;

          then (K (/\) B) = ( EmptyMS I) by A1;

          then ((K . i) /\ (B . i)) = (( EmptyMS I) . i) by A2, PBOOLE:def 5;

          then (X9 /\ (B . i)) = {} by A6, PBOOLE: 5;

          hence thesis by XBOOLE_0:def 7;

        end;

        then ( union (A . i)) misses (B . i) by ZFMISC_1: 80;

        then (( union (A . i)) /\ (B . i)) = {} by XBOOLE_0:def 7;

        then ((( union A) . i) /\ (B . i)) = {} by A2, Def2;

        then ((( union A) (/\) B) . i) = {} by A2, PBOOLE:def 5;

        hence ((( union A) (/\) B) . i) = (( EmptyMS I) . i) by PBOOLE: 5;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:34

    for A,B be ManySortedSet of I st (A (\/) B) is non-empty & for X,Y be ManySortedSet of I st X <> Y & X in (A (\/) B) & Y in (A (\/) B) holds (X (/\) Y) = ( EmptyMS I) holds ( union (A (/\) B)) = (( union A) (/\) ( union B))

    proof

      let A,B be ManySortedSet of I such that

       A1: (A (\/) B) is non-empty;

      assume

       A2: for X,Y be ManySortedSet of I st X <> Y & X in (A (\/) B) & Y in (A (\/) B) holds (X (/\) Y) = ( EmptyMS I);

      now

        let i be object such that

         A3: i in I;

        for X9,Y9 be set st X9 <> Y9 & X9 in ((A . i) \/ (B . i)) & Y9 in ((A . i) \/ (B . i)) holds X9 misses Y9

        proof

          consider M be ManySortedSet of I such that

           A4: M in (A (\/) B) by A1, PBOOLE: 134;

          

           A5: i in {i} by TARSKI:def 1;

          let X9,Y9 be set such that

           A6: X9 <> Y9 and

           A7: X9 in ((A . i) \/ (B . i)) and

           A8: Y9 in ((A . i) \/ (B . i));

          ( dom (M +* (i .--> X9))) = I & ( dom (M +* (i .--> Y9))) = I by A3, Lm1;

          then

          reconsider Kx = (M +* (i .--> X9)), Ky = (M +* (i .--> Y9)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

          ( dom (i .--> Y9)) = {i};

          

          then

           A10: (Ky . i) = ((i .--> Y9) . i) by A5, FUNCT_4: 13

          .= Y9 by FUNCOP_1: 72;

          

           A11: Ky in (A (\/) B)

          proof

            let j be object such that

             A12: j in I;

            now

              per cases ;

                suppose j = i;

                hence thesis by A8, A10, A12, PBOOLE:def 4;

              end;

                suppose j <> i;

                then not j in ( dom (i .--> Y9)) by TARSKI:def 1;

                then (Ky . j) = (M . j) by FUNCT_4: 11;

                hence thesis by A4, A12;

              end;

            end;

            hence thesis;

          end;

          ( dom (i .--> X9)) = {i};

          

          then

           A14: (Kx . i) = ((i .--> X9) . i) by A5, FUNCT_4: 13

          .= X9 by FUNCOP_1: 72;

          Kx in (A (\/) B)

          proof

            let j be object such that

             A15: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A7, A14, A15, PBOOLE:def 4;

              end;

                case j <> i;

                then not j in ( dom (i .--> X9)) by TARSKI:def 1;

                then (Kx . j) = (M . j) by FUNCT_4: 11;

                hence thesis by A4, A15;

              end;

            end;

            hence thesis;

          end;

          then (Kx (/\) Ky) = ( EmptyMS I) by A2, A6, A14, A10, A11;

          then ((Kx (/\) Ky) . i) = {} by PBOOLE: 5;

          then (X9 /\ Y9) = {} by A3, A14, A10, PBOOLE:def 5;

          hence thesis by XBOOLE_0:def 7;

        end;

        then ( union ((A . i) /\ (B . i))) = (( union (A . i)) /\ ( union (B . i))) by ZFMISC_1: 83;

        then ( union ((A . i) /\ (B . i))) = ((( union A) . i) /\ ( union (B . i))) by A3, Def2;

        then ( union ((A . i) /\ (B . i))) = ((( union A) . i) /\ (( union B) . i)) by A3, Def2;

        then ( union ((A . i) /\ (B . i))) = ((( union A) (/\) ( union B)) . i) by A3, PBOOLE:def 5;

        hence (( union (A (/\) B)) . i) = ((( union A) (/\) ( union B)) . i) by A3, Lm7;

      end;

      hence thesis;

    end;

    theorem :: MBOOLEAN:35

    for A,X be ManySortedSet of I holds for B be non-empty ManySortedSet of I holds (X c= ( union (A (\/) B)) & for Y be ManySortedSet of I st Y in B holds (Y (/\) X) = ( EmptyMS I)) implies X c= ( union A)

    proof

      let A,X be ManySortedSet of I, B be non-empty ManySortedSet of I;

      assume that

       A1: X c= ( union (A (\/) B)) and

       A2: for Y be ManySortedSet of I st Y in B holds (Y (/\) X) = ( EmptyMS I);

      let i be object;

      assume

       A3: i in I;

      

       A4: for Y9 be set st Y9 in (B . i) holds Y9 misses (X . i)

      proof

        consider M be ManySortedSet of I such that

         A5: M in B by PBOOLE: 134;

        let Y9 be set such that

         A6: Y9 in (B . i);

        ( dom (M +* (i .--> Y9))) = I by A3, Lm1;

        then

        reconsider K = (M +* (i .--> Y9)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        

         A7: ( dom (i .--> Y9)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A8: (K . i) = ((i .--> Y9) . i) by A7, FUNCT_4: 13

        .= Y9 by FUNCOP_1: 72;

        K in B

        proof

          let j be object such that

           A9: j in I;

          now

            per cases ;

              case j = i;

              hence thesis by A6, A8;

            end;

              case j <> i;

              then not j in ( dom (i .--> Y9)) by TARSKI:def 1;

              then (K . j) = (M . j) by FUNCT_4: 11;

              hence thesis by A5, A9;

            end;

          end;

          hence thesis;

        end;

        then (K (/\) X) = ( EmptyMS I) by A2;

        then ((K (/\) X) . i) = {} by PBOOLE: 5;

        then (Y9 /\ (X . i)) = {} by A3, A8, PBOOLE:def 5;

        hence thesis by XBOOLE_0:def 7;

      end;

      (X . i) c= (( union (A (\/) B)) . i) by A1, A3;

      then (X . i) c= ( union ((A . i) \/ (B . i))) by A3, Lm6;

      then (X . i) c= ( union (A . i)) by A4, SETFAM_1: 42;

      hence thesis by A3, Def2;

    end;

    theorem :: MBOOLEAN:36

    for A be finite-yielding non-empty ManySortedSet of I st (for X,Y be ManySortedSet of I st X in A & Y in A holds X c= Y or Y c= X) holds ( union A) in A

    proof

      let A be finite-yielding non-empty ManySortedSet of I such that

       A1: for X,Y be ManySortedSet of I st X in A & Y in A holds X c= Y or Y c= X;

      let i be object;

      assume

       A2: i in I;

      then i in ( dom A) by PARTFUN1:def 2;

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

      then

       A3: (A . i) is finite by FINSET_1:def 2;

      

       A4: for X9,Y9 be set st X9 in (A . i) & Y9 in (A . i) holds X9 c= Y9 or Y9 c= X9

      proof

        let X9,Y9 be set such that

         A5: X9 in (A . i) and

         A6: Y9 in (A . i);

        consider M be ManySortedSet of I such that

         A7: M in A by PBOOLE: 134;

        ( dom (M +* (i .--> Y9))) = I & ( dom (M +* (i .--> X9))) = I by A2, Lm1;

        then

        reconsider K1 = (M +* (i .--> X9)), K2 = (M +* (i .--> Y9)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        assume

         A8: not X9 c= Y9;

        

         A9: i in {i} by TARSKI:def 1;

        ( dom (i .--> Y9)) = {i};

        

        then

         A11: (K2 . i) = ((i .--> Y9) . i) by A9, FUNCT_4: 13

        .= Y9 by FUNCOP_1: 72;

        

         A12: K2 in A

        proof

          let j be object such that

           A13: j in I;

          per cases ;

            suppose j = i;

            hence thesis by A6, A11;

          end;

            suppose j <> i;

            then not j in ( dom (i .--> Y9)) by TARSKI:def 1;

            then (K2 . j) = (M . j) by FUNCT_4: 11;

            hence thesis by A7, A13;

          end;

        end;

        ( dom (i .--> X9)) = {i};

        

        then

         A15: (K1 . i) = ((i .--> X9) . i) by A9, FUNCT_4: 13

        .= X9 by FUNCOP_1: 72;

        K1 in A

        proof

          let j be object such that

           A16: j in I;

          per cases ;

            suppose j = i;

            hence thesis by A5, A15;

          end;

            suppose j <> i;

            then not j in ( dom (i .--> X9)) by TARSKI:def 1;

            then (K1 . j) = (M . j) by FUNCT_4: 11;

            hence thesis by A7, A16;

          end;

        end;

        then K1 c= K2 or K2 c= K1 by A1, A12;

        hence thesis by A2, A8, A15, A11;

      end;

      (A . i) <> {} by A2, PBOOLE:def 13;

      then ( union (A . i)) in (A . i) by A3, A4, CARD_2: 62;

      hence thesis by A2, Def2;

    end;