partit_2.miz

    begin

    reserve Y for non empty set,

a for Function of Y, BOOLEAN ,

G for Subset of ( PARTITIONS Y),

P,Q for a_partition of Y;

    definition

      let Y be non empty set, G be non empty Subset of ( PARTITIONS Y);

      :: original: Element

      redefine

      mode Element of G -> a_partition of Y ;

      coherence

      proof

        let p be Element of G;

        thus thesis by PARTIT1:def 3;

      end;

    end

    theorem :: PARTIT_2:1



     Th1: ( '/\' ( {} ( PARTITIONS Y))) = ( %O Y)

    proof

      for x be set holds x in ( %O Y) iff ex h be Function, F be Subset-Family of Y st ( dom h) = ( {} ( PARTITIONS Y)) & ( rng h) = F & (for d be set st d in ( {} ( PARTITIONS Y)) holds (h . d) in d) & x = ( Intersect F) & x <> {}

      proof

        let x be set;

        hereby

          reconsider h = {} as Function;

          assume x in ( %O Y);

          then

           A1: x in {Y} by PARTIT1:def 8;

          take h, F = ( {} ( bool Y));

          thus ( dom h) = ( {} ( PARTITIONS Y));

          thus ( rng h) = F;

          thus for d be set st d in ( {} ( PARTITIONS Y)) holds (h . d) in d;

          x = Y by A1, TARSKI:def 1;

          hence x = ( Intersect F) by SETFAM_1:def 9;

          thus x <> {} by A1, TARSKI:def 1;

        end;

        given h be Function, F be Subset-Family of Y such that

         A2: ( dom h) = ( {} ( PARTITIONS Y)) & ( rng h) = F and for d be set st d in ( {} ( PARTITIONS Y)) holds (h . d) in d and

         A3: x = ( Intersect F) and x <> {} ;

        F = {} by A2, RELAT_1: 42;

        then x = Y by A3, SETFAM_1:def 9;

        then x in {Y} by TARSKI:def 1;

        hence thesis by PARTIT1:def 8;

      end;

      hence thesis by BVFUNC_2:def 1;

    end;

    theorem :: PARTIT_2:2



     Th2: for R,S be Equivalence_Relation of Y holds (R \/ S) c= (R * S)

    proof

      let R,S be Equivalence_Relation of Y;

      let x,y be Element of Y;

      assume

       A1: [x, y] in (R \/ S);

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: [x, y] in R;

         [y, y] in S by EQREL_1: 5;

        hence thesis by A2, RELAT_1:def 8;

      end;

        suppose

         A3: [x, y] in S;

         [x, x] in R by EQREL_1: 5;

        hence thesis by A3, RELAT_1:def 8;

      end;

    end;

    theorem :: PARTIT_2:3

    for R be Relation of Y holds R c= ( nabla Y);

    theorem :: PARTIT_2:4



     Th4: for R be Equivalence_Relation of Y holds (( nabla Y) * R) = ( nabla Y) & (R * ( nabla Y)) = ( nabla Y)

    proof

      let R be Equivalence_Relation of Y;

      (( nabla Y) \/ R) c= (( nabla Y) * R) by Th2;

      then ( nabla Y) c= (( nabla Y) * R) by EQREL_1: 1;

      hence (( nabla Y) * R) = ( nabla Y);

      (( nabla Y) \/ R) c= (R * ( nabla Y)) by Th2;

      then ( nabla Y) c= (R * ( nabla Y)) by EQREL_1: 1;

      hence thesis;

    end;

    theorem :: PARTIT_2:5



     Th5: for P be a_partition of Y, x,y be Element of Y holds [x, y] in ( ERl P) iff x in ( EqClass (y,P))

    proof

      let P be a_partition of Y, x,y be Element of Y;

      hereby

        assume [x, y] in ( ERl P);

        then ex A be Subset of Y st A in P & x in A & y in A by PARTIT1:def 6;

        hence x in ( EqClass (y,P)) by EQREL_1:def 6;

      end;

      y in ( EqClass (y,P)) by EQREL_1:def 6;

      hence thesis by PARTIT1:def 6;

    end;

    theorem :: PARTIT_2:6

    for P,Q,R be a_partition of Y st ( ERl R) = (( ERl P) * ( ERl Q)) holds for x,y be Element of Y holds x in ( EqClass (y,R)) iff ex z be Element of Y st x in ( EqClass (z,P)) & z in ( EqClass (y,Q))

    proof

      let P,Q,R be a_partition of Y such that

       A1: ( ERl R) = (( ERl P) * ( ERl Q));

      let x,y be Element of Y;

      hereby

        assume x in ( EqClass (y,R));

        then [x, y] in ( ERl R) by Th5;

        then

        consider z be Element of Y such that

         A2: [x, z] in ( ERl P) and

         A3: [z, y] in ( ERl Q) by A1, RELSET_1: 28;

        take z;

        thus x in ( EqClass (z,P)) by A2, Th5;

        thus z in ( EqClass (y,Q)) by A3, Th5;

      end;

      given z be Element of Y such that

       A4: x in ( EqClass (z,P)) & z in ( EqClass (y,Q));

       [x, z] in ( ERl P) & [z, y] in ( ERl Q) by A4, Th5;

      then [x, y] in ( ERl R) by A1, RELAT_1:def 8;

      hence thesis by Th5;

    end;

    theorem :: PARTIT_2:7



     Th7: for R,S be Relation, Y be set st R is_reflexive_in Y & S is_reflexive_in Y holds (R * S) is_reflexive_in Y

    proof

      let R,S be Relation, Y be set such that

       A1: R is_reflexive_in Y & S is_reflexive_in Y;

      let x be object;

      assume x in Y;

      then [x, x] in R & [x, x] in S by A1;

      hence thesis by RELAT_1:def 8;

    end;

    theorem :: PARTIT_2:8



     Th8: for R be Relation, Y be set st R is_reflexive_in Y holds Y c= ( field R)

    proof

      let R be Relation, Y be set such that

       A1: R is_reflexive_in Y;

      let x be object;

      assume x in Y;

      then [x, x] in R by A1;

      hence thesis by RELAT_1: 15;

    end;

    theorem :: PARTIT_2:9



     Th9: for Y be set, R be Relation of Y st R is_reflexive_in Y holds Y = ( field R)

    proof

      let Y be set, R be Relation of Y;

      assume R is_reflexive_in Y;

      hence Y c= ( field R) by Th8;

      ( field R) c= (Y \/ Y) by RELSET_1: 8;

      hence thesis;

    end;

    theorem :: PARTIT_2:10

    for R,S be Equivalence_Relation of Y st (R * S) = (S * R) holds (R * S) is Equivalence_Relation of Y

    proof

      let R,S be Equivalence_Relation of Y such that

       A1: (R * S) = (S * R);



       A2: ( field S) = Y by ORDERS_1: 12;

      then

       A3: S is_reflexive_in Y by RELAT_2:def 9;



       A4: ( field R) = Y by ORDERS_1: 12;

      then R is_reflexive_in Y by RELAT_2:def 9;

      then (R * S) is_reflexive_in Y by A3, Th7;

      then

       A5: ( field (R * S)) = Y & ( dom (R * S)) = Y by ORDERS_1: 13;



       A6: (R * S) is_symmetric_in Y

      proof



         A7: S is_symmetric_in Y by A2, RELAT_2:def 11;

        let x,y be object such that

         A8: x in Y and

         A9: y in Y;

        assume [x, y] in (R * S);

        then

        consider z be object such that

         A10: [x, z] in R and

         A11: [z, y] in S by RELAT_1:def 8;

        z in ( field S) by A11, RELAT_1: 15;

        then

         A12: [y, z] in S by A2, A7, A9, A11;



         A13: R is_symmetric_in Y by A4, RELAT_2:def 11;

        z in ( field R) by A10, RELAT_1: 15;

        then [z, x] in R by A4, A13, A8, A10;

        hence thesis by A1, A12, RELAT_1:def 8;

      end;



       A14: (R * R) c= R & (S * S) c= S by RELAT_2: 27;

      ((R * S) * (R * S)) = (((R * S) * R) * S) by RELAT_1: 36

      .= ((R * (R * S)) * S) by A1, RELAT_1: 36

      .= (((R * R) * S) * S) by RELAT_1: 36

      .= ((R * R) * (S * S)) by RELAT_1: 36;

      then ((R * S) * (R * S)) c= (R * S) by A14, RELAT_1: 31;

      hence thesis by A5, A6, PARTFUN1:def 2, RELAT_2: 27, RELAT_2:def 11;

    end;

    begin

    theorem :: PARTIT_2:11



     Th11: for a,b be Function of Y, BOOLEAN st a '<' b holds ( 'not' b) '<' ( 'not' a)

    proof

      let a,b be Function of Y, BOOLEAN such that

       A1: a '<' b;

      let x be Element of Y;

      assume

       A2: (( 'not' b) . x) = TRUE ;

      (b . x) = (( 'not' ( 'not' b)) . x)

      .= ( 'not' TRUE ) by A2, MARGREL1:def 19

      .= FALSE ;

      then (a . x) <> TRUE by A1;

      then (a . x) = FALSE by XBOOLEAN:def 3;



      hence (( 'not' a) . x) = ( 'not' FALSE ) by MARGREL1:def 19

      .= TRUE ;

    end;

    theorem :: PARTIT_2:12



     Th12: for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), P be a_partition of Y st a '<' b holds ( All (a,P,G)) '<' ( All (b,P,G))

    proof

      let a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), P be a_partition of Y such that

       A1: a '<' b;

      let x be Element of Y;

      assume

       A2: (( All (a,P,G)) . x) = TRUE ;



       A3: ( All (a,P,G)) = ( B_INF (a,( CompF (P,G)))) by BVFUNC_2:def 9;



       A4: for y be Element of Y st y in ( EqClass (x,( CompF (P,G)))) holds (b . y) = TRUE

      proof

        let y be Element of Y;

        assume y in ( EqClass (x,( CompF (P,G))));

        then (a . y) = TRUE by A3, A2, BVFUNC_1:def 16;

        hence thesis by A1;

      end;

      ( All (b,P,G)) = ( B_INF (b,( CompF (P,G)))) by BVFUNC_2:def 9;

      hence thesis by A4, BVFUNC_1:def 16;

    end;

    theorem :: PARTIT_2:13

    for a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), P be a_partition of Y st a '<' b holds ( Ex (a,P,G)) '<' ( Ex (b,P,G))

    proof

      let a,b be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), P be a_partition of Y;



       A1: ( Ex (b,P,G)) = ( Ex (( 'not' ( 'not' b)),P,G))

      .= ( 'not' ( All (( 'not' b),P,G))) by BVFUNC_2: 18;

      assume a '<' b;

      then ( 'not' b) '<' ( 'not' a) by Th11;

      then

       A2: ( All (( 'not' b),P,G)) '<' ( All (( 'not' a),P,G)) by Th12;

      ( Ex (a,P,G)) = ( Ex (( 'not' ( 'not' a)),P,G))

      .= ( 'not' ( All (( 'not' a),P,G))) by BVFUNC_2: 18;

      hence thesis by A1, A2, Th11;

    end;

    begin



     Lm1: G is independent implies for P,Q be Subset of ( PARTITIONS Y) st P c= G & Q c= G holds (( ERl ( '/\' P)) * ( ERl ( '/\' Q))) c= (( ERl ( '/\' Q)) * ( ERl ( '/\' P)))

    proof

      assume

       A1: G is independent;

      let P,Q be Subset of ( PARTITIONS Y) such that

       A2: P c= G and

       A3: Q c= G;

      per cases ;

        suppose P = {} ;

        then P = ( {} ( PARTITIONS Y));



        then (( ERl ( '/\' Q)) * ( ERl ( '/\' P))) = (( ERl ( '/\' Q)) * ( ERl ( %O Y))) by Th1

        .= (( ERl ( '/\' Q)) * ( nabla Y)) by PARTIT1: 33

        .= ( nabla Y) by Th4;

        hence thesis;

      end;

        suppose Q = {} ;

        then Q = ( {} ( PARTITIONS Y));



        then (( ERl ( '/\' Q)) * ( ERl ( '/\' P))) = (( ERl ( %O Y)) * ( ERl ( '/\' P))) by Th1

        .= (( nabla Y) * ( ERl ( '/\' P))) by PARTIT1: 33

        .= ( nabla Y) by Th4;

        hence thesis;

      end;

        suppose

         A4: P <> {} & Q <> {} ;

        then

        reconsider G9 = G as non empty Subset of ( PARTITIONS Y) by A2;

        let x,y be Element of Y;

        assume [x, y] in (( ERl ( '/\' P)) * ( ERl ( '/\' Q)));

        then

        consider z be Element of Y such that

         A5: [x, z] in ( ERl ( '/\' P)) and

         A6: [z, y] in ( ERl ( '/\' Q)) by RELSET_1: 28;

        consider A be Subset of Y such that

         A7: A in ( '/\' P) and

         A8: x in A and

         A9: z in A by A5, PARTIT1:def 6;

        consider B be Subset of Y such that

         A10: B in ( '/\' Q) and

         A11: z in B and

         A12: y in B by A6, PARTIT1:def 6;

        consider hQ be Function, FQ be Subset-Family of Y such that

         A13: ( dom hQ) = Q & ( rng hQ) = FQ and

         A14: for d be set st d in Q holds (hQ . d) in d and

         A15: B = ( Intersect FQ) and B <> {} by A10, BVFUNC_2:def 1;

        consider hP be Function, FP be Subset-Family of Y such that

         A16: ( dom hP) = P & ( rng hP) = FP and

         A17: for d be set st d in P holds (hP . d) in d and

         A18: A = ( Intersect FP) and A <> {} by A7, BVFUNC_2:def 1;

        reconsider P, Q as non empty Subset of ( PARTITIONS Y) by A4;

        deffunc P( Element of P) = ( EqClass (y,$1));

        consider hP9 be Function of P, ( bool Y) such that

         A19: for p be Element of P holds (hP9 . p) = P(p) from FUNCT_2:sch 4;

        deffunc Q( Element of Q) = ( EqClass (x,$1));

        consider hQ9 be Function of Q, ( bool Y) such that

         A20: for p be Element of Q holds (hQ9 . p) = Q(p) from FUNCT_2:sch 4;

        deffunc P( set) = $1;



         A21: for d be Element of G9 holds ( bool Y) meets P(d)

        proof

          let d be Element of G9;

          d meets d;

          hence ( bool Y) meets d by XBOOLE_1: 63;

        end;

        consider h9 be Function of G9, ( bool Y) such that

         A22: for d be Element of G9 holds (h9 . d) in P(d) from FUNCT_2:sch 10( A21);

        set h = ((h9 +* hP9) +* hQ9);



         A23: ( dom hQ9) = Q by FUNCT_2:def 1;



         A24: ( dom hP9) = P by FUNCT_2:def 1;



         A25: for d be set st d in P holds (h . d) = (hP9 . d)

        proof

          let d be set;

          assume

           A26: d in P;

          then

          reconsider d9 = d as Element of P;

          per cases ;

            suppose

             A27: d in Q;

            then

             A28: (hQ . d) in FQ by A13, FUNCT_1:def 3;

            then

             A29: y in (hQ . d) by A12, A15, SETFAM_1: 43;



             A30: z in (hQ . d) by A11, A15, A28, SETFAM_1: 43;



             A31: (hQ . d) in d by A14, A27;



             A32: (hP . d) in FP by A16, A26, FUNCT_1:def 3;

            then

             A33: x in (hP . d) by A8, A18, SETFAM_1: 43;



             A34: z in (hP . d) by A9, A18, A32, SETFAM_1: 43;



             A35: (hP . d) in d by A17, A26;



            thus (h . d) = (hQ9 . d) by A23, A27, FUNCT_4: 13

            .= ( EqClass (x,d9)) by A20, A27

            .= (hP . d) by A35, A33, EQREL_1:def 6

            .= ( EqClass (z,d9)) by A35, A34, EQREL_1:def 6

            .= (hQ . d) by A31, A30, EQREL_1:def 6

            .= ( EqClass (y,d9)) by A31, A29, EQREL_1:def 6

            .= (hP9 . d) by A19;

          end;

            suppose not d in Q;



            hence (h . d) = ((h9 +* hP9) . d) by A23, FUNCT_4: 11

            .= (hP9 . d) by A24, A26, FUNCT_4: 13;

          end;

        end;

        reconsider FP9 = ( rng hP9), FQ9 = ( rng hQ9) as Subset-Family of Y;

        set A9 = ( Intersect FP9), B9 = ( Intersect FQ9);

        for a be set st a in FP9 holds y in a

        proof

          let a be set;

          assume a in FP9;

          then

          consider b be object such that

           A36: b in ( dom hP9) and

           A37: (hP9 . b) = a by FUNCT_1:def 3;

          reconsider b as Element of P by A36;

          a = ( EqClass (y,b)) by A19, A37;

          hence thesis by EQREL_1:def 6;

        end;

        then

         A38: y in A9 by SETFAM_1: 43;

        for a be set st a in FQ9 holds x in a

        proof

          let a be set;

          assume a in FQ9;

          then

          consider b be object such that

           A39: b in ( dom hQ9) and

           A40: (hQ9 . b) = a by FUNCT_1:def 3;

          reconsider b as Element of Q by A39;

          a = ( EqClass (x,b)) by A20, A40;

          hence thesis by EQREL_1:def 6;

        end;

        then

         A41: x in B9 by SETFAM_1: 43;



         A42: for d be set st d in Q holds (hQ9 . d) in d

        proof

          let d be set;

          assume d in Q;

          then

          reconsider d as Element of Q;

          (hQ9 . d) = ( EqClass (x,d)) by A20;

          hence thesis;

        end;

        ( rng (h9 +* hP9)) c= (( rng h9) \/ ( rng hP9)) by FUNCT_4: 17;

        then ( rng (h9 +* hP9)) c= ( bool Y) by XBOOLE_1: 1;

        then ( rng h) c= (( rng (h9 +* hP9)) \/ ( rng hQ9)) & (( rng (h9 +* hP9)) \/ ( rng hQ9)) c= ( bool Y) by FUNCT_4: 17, XBOOLE_1: 8;

        then

        reconsider F = ( rng h) as Subset-Family of Y by XBOOLE_1: 1;



         A43: ( dom h) = (( dom (h9 +* hP9)) \/ Q) by A23, FUNCT_4:def 1

        .= ((( dom h9) \/ P) \/ Q) by A24, FUNCT_4:def 1

        .= ((G \/ P) \/ Q) by FUNCT_2:def 1

        .= (G \/ Q) by A2, XBOOLE_1: 12

        .= G by A3, XBOOLE_1: 12;



         A44: for d be set st d in P holds (hP9 . d) in d

        proof

          let d be set;

          assume d in P;

          then

          reconsider d as Element of P;

          (hP9 . d) = ( EqClass (y,d)) by A19;

          hence thesis;

        end;

        for d be set st d in G holds (h . d) in d

        proof

          let d be set;

          assume

           A45: d in G;

          G = ((P \/ Q) \/ G) by A2, A3, XBOOLE_1: 8, XBOOLE_1: 12

          .= ((G \ (P \/ Q)) \/ (P \/ Q)) by XBOOLE_1: 39;

          then

           A46: d in (G \ (P \/ Q)) or d in (P \/ Q) by A45, XBOOLE_0:def 3;

          per cases by A46, XBOOLE_0:def 3;

            suppose

             A47: d in Q;

            then (h . d) = (hQ9 . d) by A23, FUNCT_4: 13;

            hence thesis by A42, A47;

          end;

            suppose

             A48: d in P;

            then (h . d) = (hP9 . d) by A25;

            hence thesis by A44, A48;

          end;

            suppose

             A49: d in (G \ (P \/ Q));

            then not d in (P \/ Q) by XBOOLE_0:def 5;

            then h = (h9 +* (hP9 +* hQ9)) & not d in ( dom (hP9 +* hQ9)) by A24, A23, FUNCT_4: 14, FUNCT_4:def 1;

            then

             A50: (h . d) = (h9 . d) by FUNCT_4: 11;

            d in G by A49, XBOOLE_0:def 5;

            hence thesis by A22, A50;

          end;

        end;

        then ( Intersect F) <> {} by A1, A43, BVFUNC_2:def 5;

        then

        consider t be Element of Y such that

         A51: t in ( Intersect F) by SUBSET_1: 4;

        for a be set st a in FP9 holds t in a

        proof

          let a be set;

          assume a in FP9;

          then

          consider b be object such that

           A52: b in ( dom hP9) and

           A53: (hP9 . b) = a by FUNCT_1:def 3;

          (hP9 . b) = (h . b) by A25, A52;

          then a in F by A2, A24, A43, A52, A53, FUNCT_1:def 3;

          hence thesis by A51, SETFAM_1: 43;

        end;

        then

         A54: t in A9 by SETFAM_1: 43;

        then A9 in ( '/\' P) by A44, A24, BVFUNC_2:def 1;

        then

         A55: [t, y] in ( ERl ( '/\' P)) by A38, A54, PARTIT1:def 6;

        for a be set st a in FQ9 holds t in a

        proof

          let a be set;

          assume a in FQ9;

          then

          consider b be object such that

           A56: b in ( dom hQ9) and

           A57: (hQ9 . b) = a by FUNCT_1:def 3;

          reconsider b as Element of Q by A56;

          (hQ9 . b) = (h . b) by A56, FUNCT_4: 13;

          then a in F by A3, A23, A43, A56, A57, FUNCT_1:def 3;

          hence thesis by A51, SETFAM_1: 43;

        end;

        then

         A58: t in B9 by SETFAM_1: 43;

        then B9 in ( '/\' Q) by A42, A23, BVFUNC_2:def 1;

        then [x, t] in ( ERl ( '/\' Q)) by A41, A58, PARTIT1:def 6;

        hence thesis by A55, RELSET_1: 28;

      end;

    end;

    theorem :: PARTIT_2:14



     Th14: G is independent implies for P,Q be Subset of ( PARTITIONS Y) st P c= G & Q c= G holds (( ERl ( '/\' P)) * ( ERl ( '/\' Q))) = (( ERl ( '/\' Q)) * ( ERl ( '/\' P))) by Lm1;

    theorem :: PARTIT_2:15



     Th15: G is independent implies ( All (( All (a,P,G)),Q,G)) = ( All (( All (a,Q,G)),P,G))

    proof

      set A = (G \ {P}), B = (G \ {Q});



       A1: ( CompF (P,G)) = ( '/\' A) by BVFUNC_2:def 7;



       A2: A c= G & B c= G by XBOOLE_1: 36;



       A3: ( CompF (Q,G)) = ( '/\' B) by BVFUNC_2:def 7;

      assume G is independent;

      then

       A4: (( ERl ( '/\' A)) * ( ERl ( '/\' B))) = (( ERl ( '/\' B)) * ( ERl ( '/\' A))) by A2, Th14;



       A5: for y be Element of Y holds ((for x be Element of Y st x in ( EqClass (y,( CompF (Q,G)))) holds (( B_INF (a,( CompF (P,G)))) . x) = TRUE ) implies (( B_INF (( B_INF (a,( CompF (Q,G)))),( CompF (P,G)))) . y) = TRUE ) & ( not (for x be Element of Y st x in ( EqClass (y,( CompF (Q,G)))) holds (( B_INF (a,( CompF (P,G)))) . x) = TRUE ) implies (( B_INF (( B_INF (a,( CompF (Q,G)))),( CompF (P,G)))) . y) = FALSE )

      proof

        let y be Element of Y;

        hereby

          assume

           A6: for x be Element of Y st x in ( EqClass (y,( CompF (Q,G)))) holds (( B_INF (a,( CompF (P,G)))) . x) = TRUE ;

          for x be Element of Y st x in ( EqClass (y,( CompF (P,G)))) holds (( B_INF (a,( CompF (Q,G)))) . x) = TRUE

          proof

            let x be Element of Y;

            assume x in ( EqClass (y,( CompF (P,G))));

            then

             A7: [x, y] in ( ERl ( '/\' A)) by A1, Th5;

            for z be Element of Y st z in ( EqClass (x,( CompF (Q,G)))) holds (a . z) = TRUE

            proof

              let z be Element of Y;

              assume z in ( EqClass (x,( CompF (Q,G))));

              then [z, x] in ( ERl ( '/\' B)) by A3, Th5;

              then [z, y] in (( ERl ( '/\' A)) * ( ERl ( '/\' B))) by A4, A7, RELAT_1:def 8;

              then

              consider u be object such that

               A8: [z, u] in ( ERl ( '/\' A)) and

               A9: [u, y] in ( ERl ( '/\' B)) by RELAT_1:def 8;

              u in ( field ( ERl ( '/\' B))) by A9, RELAT_1: 15;

              then

              reconsider u as Element of Y by ORDERS_1: 12;

              u in ( EqClass (y,( CompF (Q,G)))) by A3, A9, Th5;

              then

               A10: (( B_INF (a,( CompF (P,G)))) . u) <> FALSE by A6;

              z in ( EqClass (u,( CompF (P,G)))) by A1, A8, Th5;

              hence thesis by A10, BVFUNC_1:def 16;

            end;

            hence thesis by BVFUNC_1:def 16;

          end;

          hence (( B_INF (( B_INF (a,( CompF (Q,G)))),( CompF (P,G)))) . y) = TRUE by BVFUNC_1:def 16;

        end;

        given x be Element of Y such that

         A11: x in ( EqClass (y,( CompF (Q,G)))) and

         A12: (( B_INF (a,( CompF (P,G)))) . x) <> TRUE ;

        consider z be Element of Y such that

         A13: z in ( EqClass (x,( CompF (P,G)))) and

         A14: (a . z) <> TRUE by A12, BVFUNC_1:def 16;



         A15: [x, y] in ( ERl ( '/\' B)) by A3, A11, Th5;

         [z, x] in ( ERl ( '/\' A)) by A1, A13, Th5;

        then [z, y] in (( ERl ( '/\' B)) * ( ERl ( '/\' A))) by A4, A15, RELAT_1:def 8;

        then

        consider u be object such that

         A16: [z, u] in ( ERl ( '/\' B)) and

         A17: [u, y] in ( ERl ( '/\' A)) by RELAT_1:def 8;

        u in ( field ( ERl ( '/\' B))) by A16, RELAT_1: 15;

        then

        reconsider u as Element of Y by ORDERS_1: 12;

        z in ( EqClass (u,( CompF (Q,G)))) by A3, A16, Th5;

        then

         A18: (( B_INF (a,( CompF (Q,G)))) . u) = FALSE by A14, BVFUNC_1:def 16;

        u in ( EqClass (y,( CompF (P,G)))) by A1, A17, Th5;

        hence thesis by A18, BVFUNC_1:def 16;

      end;



      thus ( All (( All (a,P,G)),Q,G)) = ( B_INF (( All (a,P,G)),( CompF (Q,G)))) by BVFUNC_2:def 9

      .= ( B_INF (( B_INF (a,( CompF (P,G)))),( CompF (Q,G)))) by BVFUNC_2:def 9

      .= ( B_INF (( B_INF (a,( CompF (Q,G)))),( CompF (P,G)))) by A5, BVFUNC_1:def 16

      .= ( B_INF (( All (a,Q,G)),( CompF (P,G)))) by BVFUNC_2:def 9

      .= ( All (( All (a,Q,G)),P,G)) by BVFUNC_2:def 9;

    end;

    theorem :: PARTIT_2:16

    G is independent implies ( Ex (( Ex (a,P,G)),Q,G)) = ( Ex (( Ex (a,Q,G)),P,G))

    proof

      assume

       A1: G is independent;



      thus ( Ex (( Ex (a,P,G)),Q,G)) = ( 'not' ( 'not' ( Ex (( Ex (a,P,G)),Q,G))))

      .= ( 'not' ( All (( 'not' ( Ex (a,P,G))),Q,G))) by BVFUNC_2: 19

      .= ( 'not' ( All (( All (( 'not' a),P,G)),Q,G))) by BVFUNC_2: 19

      .= ( 'not' ( All (( All (( 'not' a),Q,G)),P,G))) by A1, Th15

      .= ( 'not' ( All (( 'not' ( Ex (a,Q,G))),P,G))) by BVFUNC_2: 19

      .= ( 'not' ( 'not' ( Ex (( Ex (a,Q,G)),P,G)))) by BVFUNC_2: 19

      .= ( Ex (( Ex (a,Q,G)),P,G));

    end;

    theorem :: PARTIT_2:17

    for a be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), P,Q be a_partition of Y st G is independent holds ( Ex (( All (a,P,G)),Q,G)) '<' ( All (( Ex (a,Q,G)),P,G))

    proof

      let a be Function of Y, BOOLEAN , G be Subset of ( PARTITIONS Y), P,Q be a_partition of Y such that

       A1: G is independent;

      set A = (G \ {P}), B = (G \ {Q});

      A c= G & B c= G by XBOOLE_1: 36;

      then

       A2: (( ERl ( '/\' A)) * ( ERl ( '/\' B))) = (( ERl ( '/\' B)) * ( ERl ( '/\' A))) by A1, Th14;



       A3: ( CompF (P,G)) = ( '/\' A) by BVFUNC_2:def 7;



       A4: ( Ex (( All (a,P,G)),Q,G)) = ( B_SUP (( All (a,P,G)),( CompF (Q,G)))) by BVFUNC_2:def 10;



       A5: ( CompF (Q,G)) = ( '/\' B) by BVFUNC_2:def 7;

      let x be Element of Y such that

       A6: (( Ex (( All (a,P,G)),Q,G)) . x) = TRUE ;



       A7: for z be Element of Y st z in ( EqClass (x,( CompF (P,G)))) holds (( Ex (a,Q,G)) . z) = TRUE

      proof

        let z be Element of Y;

        consider y be Element of Y such that

         A8: y in ( EqClass (x,( CompF (Q,G)))) and

         A9: (( All (a,P,G)) . y) = TRUE by A6, A4, BVFUNC_1:def 17;

        assume z in ( EqClass (x,( CompF (P,G))));

        then [z, x] in ( ERl ( '/\' A)) by A3, Th5;

        then

         A10: [x, z] in ( ERl ( '/\' A)) by EQREL_1: 6;

         [y, x] in ( ERl ( '/\' B)) by A5, A8, Th5;

        then [y, z] in (( ERl ( '/\' A)) * ( ERl ( '/\' B))) by A2, A10, RELAT_1:def 8;

        then

        consider u be object such that

         A11: [y, u] in ( ERl ( '/\' A)) and

         A12: [u, z] in ( ERl ( '/\' B)) by RELAT_1:def 8;

        u in ( field ( ERl ( '/\' B))) by A12, RELAT_1: 15;

        then

        reconsider u as Element of Y by ORDERS_1: 12;

         [u, y] in ( ERl ( '/\' A)) by A11, EQREL_1: 6;

        then ( All (a,P,G)) = ( B_INF (a,( CompF (P,G)))) & u in ( EqClass (y,( CompF (P,G)))) by A3, Th5, BVFUNC_2:def 9;

        then

         A13: (a . u) = TRUE by A9, BVFUNC_1:def 16;

        ( Ex (a,Q,G)) = ( B_SUP (a,( CompF (Q,G)))) & u in ( EqClass (z,( CompF (Q,G)))) by A5, A12, Th5, BVFUNC_2:def 10;

        hence thesis by A13, BVFUNC_1:def 17;

      end;

      ( All (( Ex (a,Q,G)),P,G)) = ( B_INF (( Ex (a,Q,G)),( CompF (P,G)))) by BVFUNC_2:def 9;

      hence thesis by A7, BVFUNC_1:def 16;

    end;

    begin

    reserve x,y,z for set,

S,X for non empty set,

R for Relation of X;

    notation

      let A,B be set;

      synonym [#] (A,B) for [:A,B:];

    end

    definition

      let A,B be set;

      :: PARTIT_2:def1

      func {} (A,B) -> Relation of A, B equals {} ;

      correctness by RELSET_1: 12;

      :: original: [#]

      redefine

      func [#] (A,B) -> Relation of A, B ;

      correctness

      proof

        ( [#] (A,B)) c= [:A, B:];

        hence thesis;

      end;

    end

    registration

      let A,B be set;

      cluster ( {} (A,B)) -> empty;

      coherence ;

    end

    theorem :: PARTIT_2:18

    ( field ( id X)) = X

    proof

      ( dom ( id X)) = X & ( rng ( id X)) = X;

      then ( field ( id X)) = (X \/ X) by RELAT_1:def 6;

      hence thesis;

    end;

    theorem :: PARTIT_2:19

     op1 = { [ {} , {} ]}

    proof

       { {} } = ( dom op1 ) by FUNCT_2:def 1;

      then {} in ( dom op1 ) by TARSKI:def 1;

      then [ {} , ( op1 . {} )] in op1 by FUNCT_1:def 2;

      then

       A1: { [ {} , ( op1 . {} )]} c= op1 by ZFMISC_1: 31;

      ( rng op1 ) = {( op1 . {} )} by FUNCT_2: 48;

      then

       A2: ( op1 . {} ) = {} by ZFMISC_1: 18;

       op1 c= [: { {} }, { {} }:];

      then op1 c= { [ {} , {} ]} by ZFMISC_1: 29;

      hence thesis by A2, A1;

    end;

    theorem :: PARTIT_2:20

    for A,B be set holds ( field ( {} (A,B))) = {} by RELAT_1: 40;

    theorem :: PARTIT_2:21

    R is_reflexive_in X implies R is reflexive & ( field R) = X by Th9;

    theorem :: PARTIT_2:22

    R is_symmetric_in X implies R is symmetric

    proof

      assume

       A1: R is_symmetric_in X;

      let x,y be object;

      ( field R) c= (X \/ X) by RELSET_1: 8;

      hence thesis by A1;

    end;

    theorem :: PARTIT_2:23

    R is symmetric implies R is_symmetric_in S

    proof

      assume R is symmetric;

      then

       A1: R is_symmetric_in ( field R);

      let x,y be object;

      assume x in S & y in S;

      assume

       A2: [x, y] in R;

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      hence thesis by A1, A2;

    end;

    theorem :: PARTIT_2:24

    R is antisymmetric implies R is_antisymmetric_in S

    proof

      assume R is antisymmetric;

      then

       A1: R is_antisymmetric_in ( field R);

      let x,y be object;

      assume x in S & y in S;

      assume

       A2: [x, y] in R;

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      hence thesis by A1, A2;

    end;

    theorem :: PARTIT_2:25

    R is_antisymmetric_in X implies R is antisymmetric

    proof

      assume

       A1: R is_antisymmetric_in X;

      let x,y be object;

      ( field R) c= (X \/ X) by RELSET_1: 8;

      hence thesis by A1;

    end;

    theorem :: PARTIT_2:26

    R is transitive implies R is_transitive_in S

    proof

      assume R is transitive;

      then

       A1: R is_transitive_in ( field R);

      let x,y,z be object;

      assume x in S & y in S & z in S;

      assume

       A2: [x, y] in R;

      then

       A3: x in ( field R) by RELAT_1: 15;

      assume

       A4: [y, z] in R;

      then y in ( field R) & z in ( field R) by RELAT_1: 15;

      hence thesis by A1, A2, A4, A3;

    end;

    theorem :: PARTIT_2:27

    R is_transitive_in X implies R is transitive

    proof

      assume

       A1: R is_transitive_in X;

      let x,y,z be object;

      ( field R) c= (X \/ X) by RELSET_1: 8;

      hence thesis by A1;

    end;

    theorem :: PARTIT_2:28

    R is asymmetric implies R is_asymmetric_in S

    proof

      assume R is asymmetric;

      then

       A1: R is_asymmetric_in ( field R);

      let x,y be object;

      assume x in S & y in S;

      assume

       A2: [x, y] in R;

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      hence thesis by A1, A2;

    end;

    theorem :: PARTIT_2:29

    R is_asymmetric_in X implies R is asymmetric

    proof

      assume

       A1: R is_asymmetric_in X;

      let x,y be object;

      ( field R) c= (X \/ X) by RELSET_1: 8;

      hence thesis by A1;

    end;

    theorem :: PARTIT_2:30

    R is irreflexive & ( field R) c= S implies R is_irreflexive_in S

    proof

      assume that

       A1: R is irreflexive and

       A2: ( field R) c= S;

      let x be object;

      S = (( field R) \/ (S \ ( field R))) by A2, XBOOLE_1: 45;

      then

       A3: x in S implies x in ( field R) or x in (S \ ( field R)) by XBOOLE_0:def 3;



       A4: x in (S \ ( field R)) implies not [x, x] in R

      proof

        assume x in (S \ ( field R));

        then x in (S \ (( dom R) \/ ( rng R))) by RELAT_1:def 6;

        then x in ((S \ ( dom R)) /\ (S \ ( rng R))) by XBOOLE_1: 53;

        then x in (S \ ( rng R)) by XBOOLE_0:def 4;

        then not x in ( rng R) by XBOOLE_0:def 5;

        hence thesis by XTUPLE_0:def 13;

      end;

      R is_irreflexive_in ( field R) by A1;

      hence thesis by A3, A4;

    end;

    theorem :: PARTIT_2:31

    R is_irreflexive_in X implies R is irreflexive

    proof



       A1: ( field R) c= (X \/ X) by RELSET_1: 8;

      assume R is_irreflexive_in X;

      then for x be object holds x in ( field R) implies not [x, x] in R by A1;

      then R is_irreflexive_in ( field R);

      hence thesis;

    end;

    registration

      cluster empty -> irreflexive asymmetric transitive for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: R is empty;

        hence for x be object holds x in ( field R) implies not [x, x] in R;

        thus for x,y be object holds x in ( field R) & y in ( field R) & [x, y] in R implies not [y, x] in R by A1;

        thus for x,y,z be object holds x in ( field R) & y in ( field R) & z in ( field R) & [x, y] in R & [y, z] in R implies [x, z] in R by A1;

      end;

    end

    definition

      let f be Function;

      :: PARTIT_2:def2

      attr f is involutive means for x be set st x in ( dom f) holds (f . (f . x)) = x;

    end

    definition

      let X;

      let f be UnOp of X;

      :: original: involutive

      redefine

      :: PARTIT_2:def3

      attr f is involutive means for x be Element of X holds (f . (f . x)) = x;

      compatibility

      proof

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

        hence f is involutive implies for x be Element of X holds (f . (f . x)) = x;

        assume

         A1: for x be Element of X holds (f . (f . x)) = x;

        let x be set;

        assume x in ( dom f);

        hence thesis by A1;

      end;

    end

    registration

      cluster op1 -> involutive;

      coherence

      proof

         op1 is involutive

        proof

          let a be Element of { 0 };

          a = {} by TARSKI:def 1;

          hence ( op1 . ( op1 . a)) = a by FUNCT_2: 50;

        end;

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster ( id X) -> involutive;

      coherence

      proof

        set f = ( id X);

        let a be set;

        assume a in ( dom f);

        then a in X;

        then (f . a) = a by FUNCT_1: 17;

        hence thesis;

      end;

    end