armstrng.miz



    begin

     Lm1:

    now

      let n be Nat, X be non empty set, t be Tuple of n, X;

      ( len t) = n by CARD_1:def 7;

      hence ( dom t) = ( Seg n) by FINSEQ_1:def 3;

    end;

     Lm2:

    now

      let n be Element of NAT , X be non empty set, t be Element of (n -tuples_on X);

      ( len t) = n by CARD_1:def 7;

      hence ( dom t) = ( Seg n) by FINSEQ_1:def 3;

    end;

    theorem :: ARMSTRNG:1

    

     Th1: for B be set st B is cap-closed holds for X be set, S be finite Subset-Family of X st X in B & S c= B holds ( Intersect S) in B

    proof

      let B be set;

      assume

       A1: B is cap-closed;

      let X be set, S be finite Subset-Family of X such that

       A2: X in B and

       A3: S c= B;

      defpred P[ set] means for sf be Subset-Family of X st sf = $1 holds ( Intersect sf) in B;

       A4:

      now

        let x be set, b be set such that

         A5: x in S and

         A6: b c= S and

         A7: P[b];

        thus P[(b \/ {x})]

        proof

          reconsider fx = {x} as Subset-Family of X by A5, ZFMISC_1: 31;

          reconsider fb = b as Subset-Family of X by A6, XBOOLE_1: 1;

          reconsider sx = x as Subset of X by A5;

          

           A8: ( Intersect (fb \/ fx)) = (( Intersect fb) /\ ( Intersect fx)) by MSSUBFAM: 8

          .= (( Intersect fb) /\ sx) by MSSUBFAM: 9;

          

           A9: ( Intersect fb) in B by A7;

          let sf be Subset-Family of X;

          assume sf = (b \/ {x});

          hence thesis by A1, A3, A5, A9, A8;

        end;

      end;

      

       A10: S is finite;

      

       A11: P[ {} ] by A2, SETFAM_1:def 9;

       P[S] from FINSET_1:sch 2( A10, A11, A4);

      hence thesis;

    end;

    registration

      cluster reflexive antisymmetric transitive non empty for Relation;

      existence

      proof

        set R = { [ {} , {} ]};

        reconsider R as Relation;

        take R;

        

         A1: ( field R) = { {} , {} } by RELAT_1: 17

        .= { {} } by ENUMSET1: 29;

        thus R is reflexive

        proof

          let x be object;

          assume x in ( field R);

          then x = {} by A1, TARSKI:def 1;

          hence thesis by TARSKI:def 1;

        end;

        thus R is antisymmetric

        proof

          let x,y be object;

          assume that

           A2: x in ( field R) and

           A3: y in ( field R) and [x, y] in R and [y, x] in R;

          x = {} by A1, A2, TARSKI:def 1;

          hence thesis by A1, A3, TARSKI:def 1;

        end;

        thus R is transitive

        proof

          let x,y,z be object;

          assume that

           A4: x in ( field R) and y in ( field R) and

           A5: z in ( field R) and [x, y] in R and [y, z] in R;

          

           A6: z = {} by A1, A5, TARSKI:def 1;

          x = {} by A1, A4, TARSKI:def 1;

          hence thesis by A6, TARSKI:def 1;

        end;

        thus thesis;

      end;

    end

    theorem :: ARMSTRNG:2

    

     Th2: for R be antisymmetric transitive non empty Relation, X be finite Subset of ( field R) st X <> {} holds ex x be Element of X st x is_maximal_wrt (X,R)

    proof

      let R be antisymmetric transitive non empty Relation, X be finite Subset of ( field R);

      reconsider IR = R as Relation of ( field R) by PRE_POLY: 18;

      set S = RelStr (# ( field R), IR #);

      set CR = the carrier of S;

      set ir = the InternalRel of S;

      

       A1: CR is non empty;

      

       A2: R is_transitive_in ( field R) by RELAT_2:def 16;

      

       A3: S is transitive

      proof

        let x,y,z be Element of S;

        assume that

         A4: x <= y and

         A5: y <= z;

        

         A6: [y, z] in ir by A5, ORDERS_2:def 5;

         [x, y] in ir by A4, ORDERS_2:def 5;

        then [x, z] in ir by A1, A2, A6;

        hence thesis by ORDERS_2:def 5;

      end;

      

       A7: R is_antisymmetric_in ( field R) by RELAT_2:def 12;

      S is antisymmetric

      proof

        let x,y be Element of S;

        assume that

         A8: x <= y and

         A9: y <= x;

        

         A10: [y, x] in ir by A9, ORDERS_2:def 5;

         [x, y] in ir by A8, ORDERS_2:def 5;

        hence thesis by A1, A7, A10;

      end;

      then

      reconsider S as antisymmetric transitive non empty RelStr by A3;

      reconsider Y = X as finite Subset of CR;

      assume X <> {} ;

      then

      consider x be Element of S such that

       A11: x in Y and

       A12: x is_maximal_wrt (Y,the InternalRel of S) by BAGORDER: 6;

      reconsider x as Element of X by A11;

      take x;

      thus x in X by A11;

      given y be set such that

       A13: y in X and

       A14: y <> x and

       A15: [x, y] in R;

      thus thesis by A12, A13, A14, A15;

    end;

    scheme :: ARMSTRNG:sch1

    SubsetSEq { X() -> set , P[ set] } :

for X1,X2 be Subset of X() st (for y be set holds y in X1 iff P[y]) & (for y be set holds y in X2 iff P[y]) holds X1 = X2;

      let X1,X2 be Subset of X() such that

       A1: for y be set holds y in X1 iff P[y] and

       A2: for y be set holds y in X2 iff P[y];

      for x be object holds x in X1 iff x in X2 by A1, A2;

      hence thesis by TARSKI: 2;

    end;

    definition

      let X be set, R be Relation;

      defpred P[ object] means $1 is_maximal_wrt (X,R);

      :: ARMSTRNG:def1

      func R Maximal_in X -> Subset of X means

      : Def1: for x be object holds x in it iff x is_maximal_wrt (X,R);

      existence

      proof

        consider I be set such that

         A1: for x be object holds x in I iff x in X & P[x] from XBOOLE_0:sch 1;

        for x be object st x in I holds x in X by A1;

        then

        reconsider I as Subset of X by TARSKI:def 3;

        take I;

        let x be object;

        thus x in I implies x is_maximal_wrt (X,R) by A1;

        assume

         A2: x is_maximal_wrt (X,R);

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of X;

        assume (for y be object holds y in X1 iff P[y]) & (for y be object holds y in X2 iff P[y]);

        then for y be object holds y in X1 iff y in X2;

        hence X1 = X2 by TARSKI: 2;

      end;

    end

    definition

      let x,X be set;

      :: ARMSTRNG:def2

      pred x is_/\-irreducible_in X means x in X & for z,y be set st z in X & y in X & x = (z /\ y) holds x = z or x = y;

    end

    notation

      let x,X be set;

      antonym x is_/\-reducible_in X for x is_/\-irreducible_in X;

    end

    definition

      let X be non empty set;

      :: ARMSTRNG:def3

      func /\-IRR X -> Subset of X means

      : Def3: for x be set holds x in it iff x is_/\-irreducible_in X;

      existence

      proof

        set irr = { z where z be Element of X : z is_/\-irreducible_in X };

        irr c= X

        proof

          let x be object;

          assume x in irr;

          then ex z be Element of X st x = z & z is_/\-irreducible_in X;

          hence thesis;

        end;

        then

        reconsider irr as Subset of X;

        take irr;

        let x be set;

        hereby

          assume x in irr;

          then ex z be Element of X st x = z & z is_/\-irreducible_in X;

          hence x is_/\-irreducible_in X;

        end;

        assume

         A1: x is_/\-irreducible_in X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ set] means $1 is_/\-irreducible_in X;

        thus for X1,X2 be Subset of X st (for y be set holds y in X1 iff P[y]) & (for y be set holds y in X2 iff P[y]) holds X1 = X2 from SubsetSEq;

      end;

    end

    scheme :: ARMSTRNG:sch2

    FinIntersect { X() -> non empty finite set , P[ set] } :

for x be set st x in X() holds P[x]

      provided

       A1: for x be set st x is_/\-irreducible_in X() holds P[x]

       and

       A2: for x,y be set st x in X() & y in X() & P[x] & P[y] holds P[(x /\ y)];

      deffunc U( set) = { x where x be Element of X() : $1 c= x };

      given x be set such that

       A3: x in X() and

       A4: not P[x];

      defpred R[ Nat] means ex s be Element of X() st ( card U(s)) = $1 & not P[s];

       U(x) c= X()

      proof

        let x1 be object;

        assume x1 in U(x);

        then ex xx be Element of X() st x1 = xx & x c= xx;

        hence thesis;

      end;

      then

      reconsider Ux = U(x) as finite set;

      

       A5: ex k be Nat st R[k]

      proof

        reconsider x as Element of X() by A3;

        take k = ( card Ux);

        take x;

        thus ( card U(x)) = k;

        thus thesis by A4;

      end;

      consider k be Nat such that

       A6: R[k] and

       A7: for n be Nat st R[n] holds k <= n from NAT_1:sch 5( A5);

      consider s be Element of X() such that

       A8: ( card U(s)) = k and

       A9: not P[s] by A6;

      per cases ;

        suppose s is_/\-irreducible_in X();

        hence contradiction by A1, A9;

      end;

        suppose

         A10: s is_/\-reducible_in X();

         U(s) c= X()

        proof

          let x be object;

          assume x in U(s);

          then ex xx be Element of X() st x = xx & s c= xx;

          hence thesis;

        end;

        then

        reconsider Us = U(s) as finite set;

        consider z,y be set such that

         A11: z in X() and

         A12: y in X() and

         A13: s = (z /\ y) and

         A14: s <> z and

         A15: s <> y by A10;

        

         A16: s c= y by A13, XBOOLE_1: 17;

         U(z) c= X()

        proof

          let x be object;

          assume x in U(z);

          then ex xx be Element of X() st x = xx & z c= xx;

          hence thesis;

        end;

        then

        reconsider Uz = U(z) as finite set;

         U(y) c= X()

        proof

          let x be object;

          assume x in U(y);

          then ex xx be Element of X() st x = xx & y c= xx;

          hence thesis;

        end;

        then

        reconsider Uy = U(y) as finite set;

        

         A17: s c= z by A13, XBOOLE_1: 17;

        reconsider y, z as Element of X() by A11, A12;

        

         A18: Uy c= Us

        proof

          let x be object;

          assume x in Uy;

          then

          consider xx be Element of X() such that

           A19: x = xx and

           A20: y c= xx;

          s c= xx by A16, A20;

          hence thesis by A19;

        end;

        now

          assume s in Uy;

          then ex x be Element of X() st s = x & y c= x;

          hence contradiction by A15, A16, XBOOLE_0:def 10;

        end;

        then Uy <> Us;

        then Uy c< Us by A18, XBOOLE_0:def 8;

        then ( card Us) > ( card Uy) by TREES_1: 6;

        then

         A21: P[y] by A7, A8;

        

         A22: Uz c= Us

        proof

          let x be object;

          assume x in Uz;

          then

          consider xx be Element of X() such that

           A23: x = xx and

           A24: z c= xx;

          s c= xx by A17, A24;

          hence thesis by A23;

        end;

        now

          assume s in Uz;

          then ex x be Element of X() st s = x & z c= x;

          hence contradiction by A14, A17, XBOOLE_0:def 10;

        end;

        then Uz <> Us;

        then Uz c< Us by A22, XBOOLE_0:def 8;

        then ( card Us) > ( card Uz) by TREES_1: 6;

        then P[z] by A7, A8;

        hence contradiction by A2, A9, A13, A21;

      end;

    end;

    theorem :: ARMSTRNG:3

    

     Th3: for X be non empty finite set, x be Element of X holds ex A be non empty Subset of X st x = ( meet A) & for s be set st s in A holds s is_/\-irreducible_in X

    proof

      let X be non empty finite set, x be Element of X;

      defpred P[ set] means ex S be non empty Subset of X st $1 = ( meet S) & for s be set st s in S holds s is_/\-irreducible_in X;

       A1:

      now

        let x,y be set such that x in X and y in X and

         A2: P[x] and

         A3: P[y];

        consider Sy be non empty Subset of X such that

         A4: y = ( meet Sy) and

         A5: for s be set st s in Sy holds s is_/\-irreducible_in X by A3;

        consider Sx be non empty Subset of X such that

         A6: x = ( meet Sx) and

         A7: for s be set st s in Sx holds s is_/\-irreducible_in X by A2;

        reconsider S = (Sx \/ Sy) as non empty Subset of X;

        now

          take S;

          thus (x /\ y) = ( meet S) by A6, A4, SETFAM_1: 9;

          let s be set;

          assume

           A8: s in S;

          per cases by A8, XBOOLE_0:def 3;

            suppose s in Sx;

            hence s is_/\-irreducible_in X by A7;

          end;

            suppose s in Sy;

            hence s is_/\-irreducible_in X by A5;

          end;

        end;

        hence P[(x /\ y)];

      end;

       A9:

      now

        let x be set;

        assume

         A10: x is_/\-irreducible_in X;

        thus P[x]

        proof

          x in X by A10;

          then

          reconsider S = {x} as non empty Subset of X by ZFMISC_1: 31;

          take S;

          thus x = ( meet S) by SETFAM_1: 10;

          let s be set;

          assume s in S;

          hence thesis by A10, TARSKI:def 1;

        end;

      end;

      for x be set st x in X holds P[x] from FinIntersect( A9, A1);

      hence thesis;

    end;

    definition

      let X be set, B be Subset-Family of X;

      :: ARMSTRNG:def4

      attr B is (B1) means X in B;

    end

    notation

      let B be set;

      synonym B is (B2) for B is cap-closed;

    end

    registration

      let X be set;

      cluster (B1) (B2) for Subset-Family of X;

      existence

      proof

        set B = {X};

        reconsider B as Subset-Family of X by ZFMISC_1: 68;

        take B;

        X in B by TARSKI:def 1;

        hence B is (B1);

        thus B is (B2)

        proof

          let a,b be set;

          assume that

           A1: a in B and

           A2: b in B;

          

           A3: b = X by A2, TARSKI:def 1;

          a = X by A1, TARSKI:def 1;

          hence thesis by A3, TARSKI:def 1;

        end;

      end;

    end

    theorem :: ARMSTRNG:4

    

     Th4: for X be set, B be non empty Subset-Family of X st B is cap-closed holds for x be Element of B st x is_/\-irreducible_in B & x <> X holds for S be finite Subset-Family of X st S c= B & x = ( Intersect S) holds x in S

    proof

      let X be set, B be non empty Subset-Family of X such that

       A1: B is (B2);

      let x be Element of B such that

       A2: x is_/\-irreducible_in B and

       A3: x <> X;

      defpred P[ set] means (ex a,b be Element of B st x <> a & x <> b & x = (a /\ b)) or ex f be Subset-Family of X st $1 = {} or $1 <> {} & $1 = f & ( Intersect f) <> x & ( Intersect f) in B;

      let S be finite Subset-Family of X such that

       A4: S c= B and

       A5: x = ( Intersect S) and

       A6: not x in S;

       A7:

      now

        let s,A be set such that

         A8: s in S and A c= S and

         A9: P[A];

        per cases by A9;

          suppose ex a,b be Element of B st x <> a & x <> b & x = (a /\ b);

          hence P[(A \/ {s})];

        end;

          suppose ex f be Subset-Family of X st A = {} or A = f & ( Intersect f) <> x & ( Intersect f) in B;

          then

          consider f be Subset-Family of X such that

           A10: A = {} or A <> {} & A = f & ( Intersect f) <> x & ( Intersect f) in B;

          thus P[(A \/ {s})]

          proof

            reconsider sf = {s} as Subset-Family of X by A8, ZFMISC_1: 31;

            

             A11: ( Intersect sf) = ( meet sf) by SETFAM_1:def 9;

            then

             A12: ( Intersect sf) = s by SETFAM_1: 10;

            per cases by A10;

              suppose A = {} ;

              hence thesis by A4, A6, A8, A12;

            end;

              suppose

               A13: A <> {} & A = f & ( Intersect f) <> x & ( Intersect f) in B;

              then

              reconsider As = (A \/ sf) as non empty Subset-Family of X by XBOOLE_1: 8;

              

               A14: ( Intersect As) = ( meet As) by SETFAM_1:def 9

              .= (( meet A) /\ ( meet sf)) by A13, SETFAM_1: 9;

              

               A15: ( Intersect f) = ( meet f) by A13, SETFAM_1:def 9;

              thus P[(A \/ {s})]

              proof

                per cases ;

                  suppose

                   A16: ( Intersect As) <> x;

                  ( Intersect As) in B by A1, A4, A8, A11, A12, A13, A15, A14;

                  hence thesis by A16;

                end;

                  suppose ( Intersect As) = x;

                  hence thesis by A4, A6, A8, A11, A12, A13, A15, A14;

                end;

              end;

            end;

          end;

        end;

      end;

      

       A17: P[ {} ];

      

       A18: S is finite;

       P[S] from FINSET_1:sch 2( A18, A17, A7);

      hence thesis by A2, A3, A5, SETFAM_1:def 9;

    end;

    definition

      let n be Element of NAT , p,q be Tuple of n, BOOLEAN ;

      :: ARMSTRNG:def5

      func p '&' q -> Tuple of n, BOOLEAN means

      : Def5: for i be set st i in ( Seg n) holds (it . i) = ((p /. i) '&' (q /. i));

      existence

      proof

        deffunc F( set) = ((p /. $1) '&' (q /. $1));

        consider z be FinSequence of BOOLEAN such that

         A1: ( len z) = n and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

        z in ( BOOLEAN * ) by FINSEQ_1:def 11;

        then z in (n -tuples_on BOOLEAN ) by A1;

        then

        reconsider z as Element of (n -tuples_on BOOLEAN );

        take z;

        let i be set;

        assume i in ( Seg n);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let it1,it2 be Tuple of n, BOOLEAN such that

         A4: for i be set st i in ( Seg n) holds (it1 . i) = ((p /. i) '&' (q /. i)) and

         A5: for i be set st i in ( Seg n) holds (it2 . i) = ((p /. i) '&' (q /. i));

        now

          

           A6: ( dom it1) = ( Seg n) by Lm1;

          hence ( dom it1) = ( dom it2) by Lm1;

          let x be object;

          assume

           A7: x in ( dom it1);

          

          hence (it1 . x) = ((p /. x) '&' (q /. x)) by A4, A6

          .= (it2 . x) by A5, A6, A7;

        end;

        hence thesis by FUNCT_1: 2;

      end;

      commutativity ;

    end

    theorem :: ARMSTRNG:5

    

     Th5: for n be Element of NAT , p be Element of (n -tuples_on BOOLEAN ) holds ((n -BinarySequence 0 ) '&' p) = (n -BinarySequence 0 )

    proof

      let n be Element of NAT , p be Element of (n -tuples_on BOOLEAN );

      set B = (n -BinarySequence 0 );

      now

        let x be object;

        

         A1: ( dom B) = ( Seg n) by Lm1;

        

         A2: ( dom (B '&' p)) = ( Seg n) by Lm1;

        hence ( dom (B '&' p)) = ( dom B) by Lm1;

        let x be object;

        assume

         A3: x in ( dom (B '&' p));

        

         A4: B = ( 0* n) by BINARI_3: 25

        .= (n |-> 0 ) by EUCLID:def 4;

        then (B . x) = 0 ;

        then (B /. x) = FALSE by A2, A3, A1, PARTFUN1:def 6;

        

        hence ((B '&' p) . x) = ( FALSE '&' (p /. x)) by A2, A3, Def5

        .= (B . x) by A4;

      end;

      hence thesis by FUNCT_1: 2;

    end;

    theorem :: ARMSTRNG:6

    for n be Element of NAT , p be Tuple of n, BOOLEAN holds (( 'not' (n -BinarySequence 0 )) '&' p) = p

    proof

      let n be Element of NAT , p be Tuple of n, BOOLEAN ;

      set B = (n -BinarySequence 0 );

      set nB = ( 'not' B);

      now

        let x be set;

        

         A1: ( dom B) = ( Seg n) by Lm1;

        

         A2: ( dom (nB '&' p)) = ( Seg n) by Lm1;

        hence

         A3: ( dom (nB '&' p)) = ( dom p) by Lm1;

        let x be object;

        assume

         A4: x in ( dom (nB '&' p));

        then

        reconsider k = x as Element of NAT ;

        B = ( 0* n) by BINARI_3: 25

        .= (n |-> 0 ) by EUCLID:def 4;

        then (B . x) = 0 ;

        then

         A5: (B /. x) = FALSE by A2, A4, A1, PARTFUN1:def 6;

        (nB /. x) = ( 'not' (B /. k)) by A2, A4, BINARITH:def 1

        .= TRUE by A5;

        

        hence ((nB '&' p) . x) = ( TRUE '&' (p /. x)) by A2, A4, Def5

        .= (p . x) by A3, A4, PARTFUN1:def 6;

      end;

      hence thesis by FUNCT_1: 2;

    end;

    theorem :: ARMSTRNG:7

    

     Th7: for n,i be Element of NAT st i < n holds ((n -BinarySequence (2 to_power i)) . (i + 1)) = 1 & for j be Element of NAT st j in ( Seg n) & j <> (i + 1) holds ((n -BinarySequence (2 to_power i)) . j) = 0

    proof

      let n,i be Element of NAT ;

      assume

       A1: i < n;

      deffunc B( Nat) = ($1 -BinarySequence (2 to_power i));

      set B = (n -BinarySequence (2 to_power i));

      defpred P[ Nat] means i < $1 implies ( B($1) . (i + 1)) = TRUE ;

       A2:

      now

        let n be Nat such that

         A3: P[n];

        now

          assume

           A4: i < (n + 1);

          then

           A5: i <= n by NAT_1: 13;

          

           A6: n in NAT by ORDINAL1:def 12;

          per cases by A5, XXREAL_0: 1;

            suppose

             A7: n = 0 ;

            ( 0* n) = (n |-> 0 ) by EUCLID:def 4;

            then ( dom ( 0* n)) = ( Seg n);

            then

             A8: ( len ( 0* n)) = n by FINSEQ_1:def 3, A6;

            ( dom <* TRUE *>) = ( Seg 1) by FINSEQ_1: 38;

            then

             A9: 1 in ( dom <* TRUE *>) by FINSEQ_1: 1;

            

             A10: i = 0 by A4, A7, NAT_1: 13;

            

            hence ( B(+) . (i + 1)) = ((( 0* n) ^ <* TRUE *>) . (i + 1)) by A7, BINARI_3: 28

            .= ( <* TRUE *> . 1) by A7, A10, A8, A9, FINSEQ_1:def 7

            .= TRUE by FINSEQ_1: 40;

          end;

            suppose

             A11: n > 0 & n = i;

            ( 0* n) = (n |-> 0 ) by EUCLID:def 4;

            then ( dom ( 0* n)) = ( Seg n);

            then

             A12: ( len ( 0* n)) = n by FINSEQ_1:def 3, A6;

            ( dom <* TRUE *>) = ( Seg 1) by FINSEQ_1: 38;

            then

             A13: 1 in ( dom <* TRUE *>) by FINSEQ_1: 1;

            

            thus ( B(+) . (i + 1)) = ((( 0* n) ^ <* TRUE *>) . (i + 1)) by A11, BINARI_3: 28

            .= ( <* TRUE *> . 1) by A11, A12, A13, FINSEQ_1:def 7

            .= TRUE by FINSEQ_1: 40;

          end;

            suppose

             A14: n > 0 & n > i;

            then

            reconsider n9 = n as non zero Nat;

            

             A15: ( 0 + 1) <= (i + 1) by XREAL_1: 6;

            (i + 1) <= n by A14, NAT_1: 13;

            then (i + 1) in ( Seg n) by A15, FINSEQ_1: 1;

            then

             A16: (i + 1) in ( dom B(n)) by Lm1;

            (2 to_power i) < (2 to_power n) by A14, POWER: 39;

            

            hence ( B(+) . (i + 1)) = (( B(n9) ^ <* FALSE *>) . (i + 1)) by BINARI_3: 27

            .= TRUE by A3, A14, A16, FINSEQ_1:def 7;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A17: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A17, A2);

      hence (B . (i + 1)) = 1 by A1;

      defpred P[ Nat] means i < $1 implies for j be Element of NAT st (i + 1) <= j & j <= $1 holds ( B($1) . (j + 1)) = FALSE ;

      let j be Element of NAT such that

       A18: j in ( Seg n) and

       A19: j <> (i + 1);

      

       A20: 1 <= j by A18, FINSEQ_1: 1;

       A21:

      now

        let n be Nat such that

         A22: P[n];

        now

          assume i < (n + 1);

          then

           A23: i <= n by NAT_1: 13;

          

           A24: ( 0 + 1) <= (i + 1) by XREAL_1: 6;

          let j be Element of NAT such that

           A25: (i + 1) <= j and

           A26: j <= (n + 1);

          per cases by A23, XXREAL_0: 1;

            suppose

             A27: n = 0 ;

            1 <= j by A25, A24, XXREAL_0: 2;

            then

             A28: j = 1 by A26, A27, XXREAL_0: 1;

            ( dom B(+)) = ( Seg (n + 1)) by Lm1;

            then not (j + 1) in ( dom B(+)) by A27, A28, FINSEQ_1: 1;

            hence ( B(+) . (j + 1)) = FALSE by FUNCT_1:def 2;

          end;

            suppose

             A29: n > 0 & n = i;

            

             A30: ( dom B(+)) = ( Seg (n + 1)) by Lm1;

            (j + 1) > (n + 1) by A25, A29, NAT_1: 13;

            then not (j + 1) in ( dom B(+)) by A30, FINSEQ_1: 1;

            hence ( B(+) . (j + 1)) = FALSE by FUNCT_1:def 2;

          end;

            suppose

             A31: n > 0 & n > i;

            then

            reconsider n9 = n as non zero Nat;

            

             A32: (2 to_power i) < (2 to_power n) by A31, POWER: 39;

            thus ( B(+) . (j + 1)) = FALSE

            proof

              j < (n + 1) or j = (n + 1) by A26, XXREAL_0: 1;

              then

               A33: j <= n or j = (n + 1) by NAT_1: 13;

              per cases by A33, XXREAL_0: 1;

                suppose j = (n + 1);

                then

                 A34: (j + 1) > (n + 1) by NAT_1: 13;

                ( dom B(+)) = ( Seg (n + 1)) by Lm1;

                then not (j + 1) in ( dom B(+)) by A34, FINSEQ_1: 1;

                hence thesis by FUNCT_1:def 2;

              end;

                suppose

                 A35: j = n;

                ( dom B(n)) = ( Seg n) by Lm1;

                then

                 A36: j = ( len B(n)) by A35, FINSEQ_1:def 3;

                ( dom <* FALSE *>) = ( Seg 1) by FINSEQ_1: 38;

                then

                 A37: 1 in ( dom <* FALSE *>) by FINSEQ_1: 1;

                

                thus ( B(+) . (j + 1)) = (( B(n9) ^ <* FALSE *>) . (j + 1)) by A32, BINARI_3: 27

                .= ( <* FALSE *> . 1) by A36, A37, FINSEQ_1:def 7

                .= FALSE by FINSEQ_1: 40;

              end;

                suppose

                 A38: j < n;

                

                 A39: 1 <= (j + 1) by NAT_1: 12;

                (j + 1) <= n by A38, NAT_1: 13;

                then (j + 1) in ( Seg n) by A39, FINSEQ_1: 1;

                then

                 A40: (j + 1) in ( dom B(n)) by Lm1;

                

                thus ( B(+) . (j + 1)) = (( B(n9) ^ <* FALSE *>) . (j + 1)) by A32, BINARI_3: 27

                .= ( B(n) . (j + 1)) by A40, FINSEQ_1:def 7

                .= FALSE by A22, A25, A31, A38;

              end;

            end;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A41: P[ 0 ];

      

       A42: for n be Nat holds P[n] from NAT_1:sch 2( A41, A21);

      defpred P[ Nat] means i < $1 implies for j be Element of NAT st 1 <= j & j < (i + 1) holds ( B($1) . j) = FALSE ;

       A43:

      now

        let n be Nat such that

         A44: P[n];

        now

          assume

           A45: i < (n + 1);

          then

           A46: i <= n by NAT_1: 13;

          let j be Element of NAT such that

           A47: 1 <= j and

           A48: j < (i + 1);

          per cases by A46, XXREAL_0: 1;

            suppose n = 0 ;

            then i = 0 by A45, NAT_1: 13;

            hence ( B(+) . j) = FALSE by A47, A48;

          end;

            suppose

             A49: n > 0 & i < n;

            then

            reconsider n9 = n as non zero Nat;

            

             A50: ( dom B(n)) = ( Seg n) by Lm1;

            

             A51: i <= n by A45, NAT_1: 13;

            j <= i by A48, NAT_1: 13;

            then j <= n by A51, XXREAL_0: 2;

            then

             A52: j in ( dom B(n)) by A47, A50, FINSEQ_1: 1;

            (2 to_power i) < (2 to_power n) by A49, POWER: 39;

            

            hence ( B(+) . j) = (( B(n9) ^ <* FALSE *>) . j) by BINARI_3: 27

            .= ( B(n) . j) by A52, FINSEQ_1:def 7

            .= FALSE by A44, A47, A48, A49;

          end;

            suppose

             A53: n > 0 & i = n;

            then j <= n by A48, NAT_1: 13;

            then

             A54: j in ( Seg n) by A47, FINSEQ_1: 1;

            

             A55: ( 0* n) = (n |-> 0 ) by EUCLID:def 4;

            then

             A56: j in ( dom ( 0* n)) by A54;

            

            thus ( B(+) . j) = ((( 0* n) ^ <* TRUE *>) . j) by A53, BINARI_3: 28

            .= (( 0* n) . j) by A56, FINSEQ_1:def 7

            .= FALSE by A55;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A57: P[ 0 ];

      

       A58: for n be Nat holds P[n] from NAT_1:sch 2( A57, A43);

      

       A59: j <= n by A18, FINSEQ_1: 1;

      per cases by A19, A59, XXREAL_0: 1;

        suppose j < (i + 1);

        hence thesis by A1, A58, A20;

      end;

        suppose

         A60: j > (i + 1) & j < n;

        then

        consider k be Nat such that

         A61: j = (k + 1) by NAT_1: 6;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A62: k <= n by A60, A61, NAT_1: 13;

        (i + 1) <= k by A60, A61, NAT_1: 13;

        hence thesis by A1, A42, A61, A62;

      end;

        suppose

         A63: j > (i + 1) & j = n;

        then

        consider m be Nat such that

         A64: n = (m + 1) by NAT_1: 6;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        i < m by A63, A64, XREAL_1: 6;

        then (2 to_power i) < (2 to_power m) by POWER: 39;

        hence thesis by A63, A64, BINARI_3: 26;

      end;

    end;

    begin

    definition

      struct DB-Rel (# the Attributes -> finite non empty set,

the Domains -> non-empty ManySortedSet of the Attributes,

the Relationship -> Subset of ( product the Domains) #)

       attr strict strict;

    end

    begin

    definition

      let X be set;

      mode Subset-Relation of X is Relation of ( bool X);

      mode Dependency-set of X is Relation of ( bool X);

    end

    registration

      let X be set;

      cluster non empty finite for Dependency-set of X;

      existence

      proof

         {} c= X;

        then

        reconsider R = { [ {} , {} ]} as Relation of ( bool X) by RELSET_1: 3;

        take R;

        thus R is non empty;

        thus thesis;

      end;

    end

    definition

      let X be set;

      :: ARMSTRNG:def6

      func Dependencies (X) -> Dependency-set of X equals [:( bool X), ( bool X):];

      coherence ;

    end

    definition

      let X be set;

      mode Dependency of X is Element of ( Dependencies X);

    end

    registration

      let X be set;

      cluster ( Dependencies X) -> non empty;

      coherence ;

    end

    definition

      let X be set, F be non empty Dependency-set of X;

      :: original: Element

      redefine

      mode Element of F -> Dependency of X ;

      correctness

      proof

        let x be Element of F;

        thus thesis;

      end;

    end

    theorem :: ARMSTRNG:8

    

     Th8: for X,x be set holds x in ( Dependencies X) iff ex a,b be Subset of X st x = [a, b]

    proof

      let X be set, x be set;

      hereby

        assume

         A1: x in ( Dependencies X);

        then

        consider a,b be object such that

         A2: [a, b] = x by RELAT_1:def 1;

        reconsider a, b as Subset of X by A1, A2, ZFMISC_1: 87;

        take a, b;

        thus x = [a, b] by A2;

      end;

      given a,b be Subset of X such that

       A3: x = [a, b];

      thus thesis by A3, ZFMISC_1: 87;

    end;

    theorem :: ARMSTRNG:9

    

     Th9: for X,x be set, F be Dependency-set of X holds x in F implies ex a,b be Subset of X st x = [a, b]

    proof

      let X,x be set, M be Dependency-set of X;

      assume

       A1: x in M;

      then

      consider a,b be object such that

       A2: [a, b] = x by RELAT_1:def 1;

      reconsider a, b as Subset of X by A1, A2, ZFMISC_1: 87;

      take a, b;

      thus thesis by A2;

    end;

    definition

      let R be DB-Rel, A,B be Subset of the Attributes of R;

      :: ARMSTRNG:def7

      pred A >|> B,R means for f,g be Element of the Relationship of R st (f | A) = (g | A) holds (f | B) = (g | B);

    end

    notation

      let R be DB-Rel, A,B be Subset of the Attributes of R;

      synonym A,B holds_in R for A >|> B,R;

    end

    definition

      let R be DB-Rel;

      :: ARMSTRNG:def8

      func Dependency-str R -> Dependency-set of the Attributes of R equals { [A, B] where A,B be Subset of the Attributes of R : A >|> (B,R) };

      coherence

      proof

        set at = the Attributes of R;

        set X = { [A, B] where A,B be Subset of the Attributes of R : A >|> (B,R) };

        X c= [:( bool at), ( bool at):]

        proof

          let x be object;

          assume x in X;

          then ex A,B be Subset of at st x = [A, B] & A >|> (B,R);

          hence thesis by ZFMISC_1:def 2;

        end;

        hence thesis;

      end;

    end

    theorem :: ARMSTRNG:10

    

     Th10: for R be DB-Rel, A,B be Subset of the Attributes of R holds [A, B] in ( Dependency-str R) iff A >|> (B,R)

    proof

      let D be DB-Rel, A,B be Subset of the Attributes of D;

      set S = ( Dependency-str D);

      hereby

        assume [A, B] in S;

        then

        consider a,b be Subset of the Attributes of D such that

         A1: [A, B] = [a, b] and

         A2: a >|> (b,D);

        A = a by A1, XTUPLE_0: 1;

        hence A >|> (B,D) by A1, A2, XTUPLE_0: 1;

      end;

      thus thesis;

    end;

    begin

    definition

      let X be set, P,Q be Dependency of X;

      :: ARMSTRNG:def9

      pred P >= Q means (P `1 ) c= (Q `1 ) & (Q `2 ) c= (P `2 );

      reflexivity ;

    end

    notation

      let X be set, P,Q be Dependency of X;

      synonym Q <= P for P >= Q;

      synonym P is_at_least_as_informative_as Q for P >= Q;

    end

    theorem :: ARMSTRNG:11

    

     Th11: for X be set, P,Q be Dependency of X st P <= Q & Q <= P holds P = Q

    proof

      let X be set, p,q be Dependency of X;

      assume that

       A1: p <= q and

       A2: q <= p;

      

       A3: (q `1 ) c= (p `1 ) by A1;

      

       A4: (p `2 ) c= (q `2 ) by A1;

      (q `2 ) c= (p `2 ) by A2;

      then

       A5: (p `2 ) = (q `2 ) by A4, XBOOLE_0:def 10;

      (p `1 ) c= (q `1 ) by A2;

      then

       A6: (p `1 ) = (q `1 ) by A3, XBOOLE_0:def 10;

      p = [(p `1 ), (p `2 )] by MCART_1: 22;

      hence thesis by A6, A5, MCART_1: 22;

    end;

    theorem :: ARMSTRNG:12

    

     Th12: for X be set, P,Q,S be Dependency of X st P <= Q & Q <= S holds P <= S

    proof

      let X be set, p,q,r be Dependency of X;

      assume that

       A1: p <= q and

       A2: q <= r;

      

       A3: (q `2 ) c= (r `2 ) by A2;

      (p `2 ) c= (q `2 ) by A1;

      then

       A4: (p `2 ) c= (r `2 ) by A3;

      

       A5: (r `1 ) c= (q `1 ) by A2;

      (q `1 ) c= (p `1 ) by A1;

      then (r `1 ) c= (p `1 ) by A5;

      hence thesis by A4;

    end;

    definition

      let X be set, A,B be Subset of X;

      :: original: [

      redefine

      func [A,B] -> Dependency of X ;

      coherence by ZFMISC_1:def 2;

    end

    theorem :: ARMSTRNG:13

    for X be set, A,B,A9,B9 be Subset of X holds [A, B] >= [A9, B9] iff A c= A9 & B9 c= B;

    definition

      let X be set;

      :: ARMSTRNG:def10

      func Dependencies-Order X -> Relation of ( Dependencies X) equals { [P, Q] where P,Q be Dependency of X : P <= Q };

      coherence

      proof

        set Y = { [E, F] where E,F be Dependency of X : E <= F };

        Y c= [:( Dependencies X), ( Dependencies X):]

        proof

          let x be object;

          assume x in Y;

          then ex E,F be Dependency of X st x = [E, F] & E <= F;

          hence thesis by ZFMISC_1:def 2;

        end;

        hence thesis;

      end;

    end

    theorem :: ARMSTRNG:14

    for X,x be set holds x in ( Dependencies-Order X) iff ex P,Q be Dependency of X st x = [P, Q] & P <= Q;

    theorem :: ARMSTRNG:15

    

     Th15: for X be set holds ( dom ( Dependencies-Order X)) = [:( bool X), ( bool X):]

    proof

      let X be set;

      now

        let x be object;

        thus x in ( dom ( Dependencies-Order X)) implies x in [:( bool X), ( bool X):];

        assume x in [:( bool X), ( bool X):];

        then

        reconsider x9 = x as Dependency of X;

         [x9, x9] in ( Dependencies-Order X);

        hence x in ( dom ( Dependencies-Order X)) by XTUPLE_0:def 12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ARMSTRNG:16

    

     Th16: for X be set holds ( rng ( Dependencies-Order X)) = [:( bool X), ( bool X):]

    proof

      let X be set;

      now

        let x be object;

        thus x in ( rng ( Dependencies-Order X)) implies x in [:( bool X), ( bool X):];

        assume x in [:( bool X), ( bool X):];

        then

        reconsider x9 = x as Dependency of X;

         [x9, x9] in ( Dependencies-Order X);

        hence x in ( rng ( Dependencies-Order X)) by XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ARMSTRNG:17

    

     Th17: for X be set holds ( field ( Dependencies-Order X)) = [:( bool X), ( bool X):]

    proof

      let X be set;

      

      thus ( field ( Dependencies-Order X)) = (( dom ( Dependencies-Order X)) \/ ( rng ( Dependencies-Order X))) by RELAT_1:def 6

      .= ( [:( bool X), ( bool X):] \/ ( rng ( Dependencies-Order X))) by Th15

      .= ( [:( bool X), ( bool X):] \/ [:( bool X), ( bool X):]) by Th16

      .= [:( bool X), ( bool X):];

    end;

    registration

      let X be set;

      cluster ( Dependencies-Order X) -> non empty;

      coherence by Th15, RELAT_1: 38;

      cluster ( Dependencies-Order X) -> total reflexive antisymmetric transitive;

      coherence

      proof

        set dx = ( Dependencies X);

        set dox = ( Dependencies-Order X);

        dx c= ( dom dox)

        proof

          let x be object;

          assume x in dx;

          then

          reconsider x9 = x as Element of dx;

          x9 <= x9;

          then [x, x] in dox;

          hence thesis by XTUPLE_0:def 12;

        end;

        then

         A1: ( dom dox) = dx by XBOOLE_0:def 10;

        

        then

         A2: ( field dox) = (dx \/ ( rng dox)) by RELAT_1:def 6

        .= dx by XBOOLE_1: 12;

        thus dox is total by A1, PARTFUN1:def 2;

        dox is_reflexive_in dx;

        hence dox is reflexive by A2;

        dox is_antisymmetric_in dx

        proof

          let x,y be object;

          assume that x in dx and y in dx and

           A3: [x, y] in dox and

           A4: [y, x] in dox;

          consider x9,y9 be Element of dx such that

           A5: [x, y] = [x9, y9] and

           A6: x9 <= y9 by A3;

          

           A7: y = y9 by A5, XTUPLE_0: 1;

          consider y99,x99 be Element of dx such that

           A8: [y, x] = [y99, x99] and

           A9: y99 <= x99 by A4;

          

           A10: x = x99 by A8, XTUPLE_0: 1;

          

           A11: y = y99 by A8, XTUPLE_0: 1;

          x = x9 by A5, XTUPLE_0: 1;

          hence thesis by A6, A9, A10, A7, A11, Th11;

        end;

        hence dox is antisymmetric by A2;

        dox is_transitive_in dx

        proof

          let x,y,z be object;

          assume that x in dx and y in dx and z in dx and

           A12: [x, y] in dox and

           A13: [y, z] in dox;

          consider x9,y9 be Element of dx such that

           A14: [x, y] = [x9, y9] and

           A15: x9 <= y9 by A12;

          

           A16: x = x9 by A14, XTUPLE_0: 1;

          consider y99,z9 be Element of dx such that

           A17: [y, z] = [y99, z9] and

           A18: y99 <= z9 by A13;

          

           A19: y = y99 by A17, XTUPLE_0: 1;

          

           A20: z = z9 by A17, XTUPLE_0: 1;

          y = y9 by A14, XTUPLE_0: 1;

          then x9 <= z9 by A15, A18, A19, Th12;

          hence thesis by A16, A20;

        end;

        hence thesis by A2;

      end;

    end

    notation

      let X be set, F be Dependency-set of X;

      synonym F is (F2) for F is transitive;

      synonym F is (DC1) for F is transitive;

    end

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def11

      attr F is (F1) means

      : Def11: for A be Subset of X holds [A, A] in F;

    end

    notation

      let X be set, F be Dependency-set of X;

      synonym F is (DC2) for F is (F1);

    end

    theorem :: ARMSTRNG:18

    

     Th18: for X be set, F be Dependency-set of X holds F is (F2) iff for A,B,C be Subset of X st [A, B] in F & [B, C] in F holds [A, C] in F

    proof

      let X be set, F be Dependency-set of X;

      hereby

        assume F is (F2);

        then

         A1: F is_transitive_in ( field F);

        let A,B,C be Subset of X;

        assume that

         A2: [A, B] in F and

         A3: [B, C] in F;

        

         A4: B in ( field F) by A2, RELAT_1: 15;

        

         A5: C in ( field F) by A3, RELAT_1: 15;

        A in ( field F) by A2, RELAT_1: 15;

        hence [A, C] in F by A1, A2, A3, A4, A5;

      end;

      assume

       A6: for A,B,C be Subset of X st [A, B] in F & [B, C] in F holds [A, C] in F;

      let x,y,z be object such that

       A7: x in ( field F) and

       A8: y in ( field F) and

       A9: z in ( field F) and

       A10: [x, y] in F and

       A11: [y, z] in F;

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

      then

      reconsider A = x, B = y, C = z as Subset of X by A7, A8, A9;

      

       A12: [B, C] in F by A11;

       [A, B] in F by A10;

      hence thesis by A6, A12;

    end;

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def12

      attr F is (F3) means

      : Def12: for A,B,A9,B9 be Subset of X st [A, B] in F & [A, B] >= [A9, B9] holds [A9, B9] in F;

      :: ARMSTRNG:def13

      attr F is (F4) means

      : Def13: for A,B,A9,B9 be Subset of X st [A, B] in F & [A9, B9] in F holds [(A \/ A9), (B \/ B9)] in F;

    end

    theorem :: ARMSTRNG:19

    

     Th19: for X be set holds ( Dependencies X) is (F1) (F2) (F3) (F4)

    proof

      let X be set;

      set D = ( Dependencies X);

      thus D is (F1);

      D = ( nabla ( bool X)) by EQREL_1:def 1;

      then

       A1: ( field D) = ( bool X) by ORDERS_1: 12;

      thus D is (F2)

      proof

        let x,y,z be object;

        assume that

         A2: x in ( field D) and y in ( field D) and

         A3: z in ( field D) and [x, y] in D and [y, z] in D;

        thus thesis by A1, A2, A3, ZFMISC_1:def 2;

      end;

      thus D is (F3);

      thus D is (F4);

    end;

    registration

      let X be set;

      cluster (F1) (F2) (F3) (F4) non empty for Dependency-set of X;

      existence

      proof

        take ( Dependencies X);

        thus thesis by Th19;

      end;

    end

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def14

      attr F is full_family means

      : Def14: F is (F1) (F2) (F3) (F4);

    end

    registration

      let X be set;

      cluster full_family for Dependency-set of X;

      existence

      proof

        set D = the (F1) (F2) (F3) (F4) non empty Dependency-set of X;

        take D;

        thus thesis;

      end;

    end

    definition

      let X be set;

      mode Full-family of X is full_family Dependency-set of X;

    end

    theorem :: ARMSTRNG:20

    for X be finite set, F be Dependency-set of X holds F is finite;

    registration

      let X be finite set;

      cluster finite for Full-family of X;

      existence

      proof

        set D = the (F1) (F2) (F3) (F4) non empty Dependency-set of X;

        reconsider D as Full-family of X by Def14;

        take D;

        thus thesis;

      end;

      cluster -> finite for Dependency-set of X;

      coherence ;

    end

    registration

      let X be set;

      cluster full_family -> (F1) (F2) (F3) (F4) for Dependency-set of X;

      coherence ;

      cluster (F1) (F2) (F3) (F4) -> full_family for Dependency-set of X;

      correctness ;

    end

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def15

      attr F is (DC3) means

      : Def15: for A,B be Subset of X st B c= A holds [A, B] in F;

    end

    registration

      let X be set;

      cluster (F1) (F3) -> (DC3) for Dependency-set of X;

      coherence

      proof

        let F be Dependency-set of X;

        assume

         A1: F is (F1) (F3);

        let A,B be Subset of X;

        assume B c= A;

        then

         A2: [A, A] >= [A, B];

        thus thesis by A1, A2;

      end;

      cluster (DC3) (F2) -> (F1) (F3) for Dependency-set of X;

      coherence

      proof

        let F be Dependency-set of X;

        assume

         A3: F is (DC3) (F2);

        thus F is (F1) by A3;

        let A,B,A9,B9 be Subset of X;

        assume

         A4: [A, B] in F;

        assume

         A5: [A, B] >= [A9, B9];

        then A c= A9;

        then [A9, A] in F by A3;

        then

         A6: [A9, B] in F by A3, A4, Th18;

        B9 c= B by A5;

        then [B, B9] in F by A3;

        hence thesis by A3, A6, Th18;

      end;

    end

    registration

      let X be set;

      cluster (DC3) (F2) (F4) non empty for Dependency-set of X;

      existence

      proof

        set D = the (F1) (F3) (F2) (F4) non empty Dependency-set of X;

        take D;

        thus thesis;

      end;

    end

    theorem :: ARMSTRNG:21

    for X be set, F be Dependency-set of X st F is (DC3) (F2) holds F is (F1) (F3);

    theorem :: ARMSTRNG:22

    for X be set, F be Dependency-set of X st F is (F1) (F3) holds F is (DC3);

    registration

      let X be set;

      cluster (F1) -> non empty for Dependency-set of X;

      coherence ;

    end

    theorem :: ARMSTRNG:23

    

     Th23: for R be DB-Rel holds ( Dependency-str R) is full_family

    proof

      let D be DB-Rel;

      set S = ( Dependency-str D);

      set T = the Attributes of D, R = the Relationship of D;

       A1:

      now

        let A,B,C be Subset of T;

        assume that

         A2: [A, B] in S and

         A3: [B, C] in S;

        

         A4: B >|> (C,D) by A3, Th10;

        

         A5: A >|> (B,D) by A2, Th10;

        A >|> (C,D)

        proof

          let f,g be Element of R;

          assume (f | A) = (g | A);

          then (f | B) = (g | B) by A5;

          hence thesis by A4;

        end;

        hence [A, C] in S;

      end;

      then

       A6: S is (F2) by Th18;

      

       A7: S is (DC3)

      proof

        let A,B be Subset of T such that

         A8: B c= A;

        A >|> (B,D)

        proof

          let f,g be Element of R such that

           A9: (f | A) = (g | A);

          

          thus (f | B) = ((f | A) | B) by A8, RELAT_1: 74

          .= (g | B) by A8, A9, RELAT_1: 74;

        end;

        hence thesis;

      end;

      hence S is (F1);

      thus S is (F2) by A1, Th18;

      thus S is (F3) by A7, A6;

      thus S is (F4)

      proof

        let A,B,A9,B9 be Subset of T;

        assume that

         A10: [A, B] in S and

         A11: [A9, B9] in S;

        

         A12: A9 >|> (B9,D) by A11, Th10;

        

         A13: A >|> (B,D) by A10, Th10;

        (A \/ A9) >|> ((B \/ B9),D)

        proof

          let f,g be Element of R;

          assume

           A14: (f | (A \/ A9)) = (g | (A \/ A9));

          (f | A9) = ((f | (A \/ A9)) | A9) by RELAT_1: 74, XBOOLE_1: 7

          .= (g | A9) by A14, RELAT_1: 74, XBOOLE_1: 7;

          then

           A15: (f | B9) = (g | B9) by A12;

          (f | A) = ((f | (A \/ A9)) | A) by RELAT_1: 74, XBOOLE_1: 7

          .= (g | A) by A14, RELAT_1: 74, XBOOLE_1: 7;

          then

           A16: (f | B) = (g | B) by A13;

          

          thus (f | (B \/ B9)) = ((f | B) \/ (f | B9)) by RELAT_1: 78

          .= (g | (B \/ B9)) by A16, A15, RELAT_1: 78;

        end;

        hence thesis;

      end;

    end;

    theorem :: ARMSTRNG:24

    for X be set, K be Subset of X holds { [A, B] where A,B be Subset of X : K c= A or B c= A } is Full-family of X

    proof

      let X be set, K be Subset of X;

      set F = { [A, B] where A,B be Subset of X : K c= A or B c= A };

      F c= [:( bool X), ( bool X):]

      proof

        let x be object;

        assume x in F;

        then ex A,B be Subset of X st x = [A, B] & (K c= A or B c= A);

        hence thesis;

      end;

      then

      reconsider F as Dependency-set of X;

      

       A1: F is (F4)

      proof

        let A,B,A9,B9 be Subset of X;

        assume that

         A2: [A, B] in F and

         A3: [A9, B9] in F;

        consider a,b be Subset of X such that

         A4: [A, B] = [a, b] and

         A5: K c= a or b c= a by A2;

        

         A6: B = b by A4, XTUPLE_0: 1;

        consider a9,b9 be Subset of X such that

         A7: [A9, B9] = [a9, b9] and

         A8: K c= a9 or b9 c= a9 by A3;

        

         A9: A9 = a9 by A7, XTUPLE_0: 1;

        

         A10: B9 = b9 by A7, XTUPLE_0: 1;

        A = a by A4, XTUPLE_0: 1;

        then K c= (A \/ A9) or (B \/ B9) c= (A \/ A9) by A5, A8, A6, A9, A10, XBOOLE_1: 10, XBOOLE_1: 13;

        hence thesis;

      end;

      now

        let A,B,C be Subset of X;

        assume that

         A11: [A, B] in F and

         A12: [B, C] in F;

        consider a,b be Subset of X such that

         A13: [A, B] = [a, b] and

         A14: K c= a or b c= a by A11;

        

         A15: A = a by A13, XTUPLE_0: 1;

        consider b1,c be Subset of X such that

         A16: [B, C] = [b1, c] and

         A17: K c= b1 or c c= b1 by A12;

        

         A18: B = b1 by A16, XTUPLE_0: 1;

        

         A19: C = c by A16, XTUPLE_0: 1;

        B = b by A13, XTUPLE_0: 1;

        then K c= a or c c= a by A14, A17, A18;

        hence [A, C] in F by A15, A19;

      end;

      then

       A20: F is (F2) by Th18;

      F is (DC3);

      hence thesis by A20, A1;

    end;

    begin

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def16

      func Maximal_wrt F -> Dependency-set of X equals (( Dependencies-Order X) Maximal_in F);

      coherence by RELSET_1: 1;

    end

    theorem :: ARMSTRNG:25

    for X be set, F be Dependency-set of X holds ( Maximal_wrt F) c= F;

    definition

      let X be set, F be Dependency-set of X, x,y be set;

      :: ARMSTRNG:def17

      pred x ^|^ y,F means [x, y] in ( Maximal_wrt F);

    end

    theorem :: ARMSTRNG:26

    

     Th26: for X be finite set, P be Dependency of X, F be Dependency-set of X st P in F holds ex A,B be Subset of X st [A, B] in ( Maximal_wrt F) & [A, B] >= P

    proof

      let X be finite set, x be Dependency of X, F be Dependency-set of X;

      set DOX = ( Dependencies-Order X);

      assume

       A1: x in F;

      then

      reconsider FF = F as non empty Dependency-set of X;

      reconsider S = { y where y be Element of FF : x <= y } as set;

      

       A2: ( field DOX) = [:( bool X), ( bool X):] by Th17;

      

       A3: S c= ( field DOX)

      proof

        let a be object;

        assume a in S;

        then ex b be Element of FF st a = b & x <= b;

        hence thesis by A2;

      end;

      x in S by A1;

      then

      consider m be Element of S such that

       A4: m is_maximal_wrt (S,DOX) by A3, Th2;

      m in S by A4;

      then

       A5: ex y be Element of FF st m = y & x <= y;

      then

      consider a,b be Subset of X such that

       A6: m = [a, b] by Th8;

      take a, b;

      m is_maximal_wrt (F,DOX)

      proof

        thus m in F by A5;

        given y be set such that

         A7: y in F and

         A8: y <> m and

         A9: [m, y] in DOX;

        consider e,f be Dependency of X such that

         A10: [m, y] = [e, f] and

         A11: e <= f by A9;

        reconsider y as Element of FF by A7;

        

         A12: y = f by A10, XTUPLE_0: 1;

        m = e by A10, XTUPLE_0: 1;

        then x <= y by A5, A11, A12, Th12;

        then y in S;

        hence contradiction by A4, A8, A9;

      end;

      hence [a, b] in ( Maximal_wrt F) by A6, Def1;

      thus thesis by A5, A6;

    end;

    theorem :: ARMSTRNG:27

    

     Th27: for X be set, F be Dependency-set of X, A,B be Subset of X holds A ^|^ (B,F) iff [A, B] in F & not ex A9,B9 be Subset of X st [A9, B9] in F & (A <> A9 or B <> B9) & [A, B] <= [A9, B9]

    proof

      let X be set, F be Dependency-set of X, x,y be Subset of X;

      set DOX = ( Dependencies-Order X);

      hereby

        assume x ^|^ (y,F);

        then

         A1: [x, y] in ( Maximal_wrt F);

        hence [x, y] in F;

        

         A2: [x, y] is_maximal_wrt (F,DOX) by A1, Def1;

        given x9,y9 be Subset of X such that

         A3: [x9, y9] in F and

         A4: x <> x9 or y <> y9 and

         A5: [x, y] <= [x9, y9];

        

         A6: [ [x, y], [x9, y9]] in DOX by A5;

         [x, y] <> [x9, y9] by A4, XTUPLE_0: 1;

        hence contradiction by A2, A3, A6;

      end;

      assume that

       A7: [x, y] in F and

       A8: not ex x9,y9 be Subset of X st [x9, y9] in F & (x <> x9 or y <> y9) & [x, y] <= [x9, y9];

       [x, y] is_maximal_wrt (F,DOX)

      proof

        thus [x, y] in F by A7;

        given z be set such that

         A9: z in F and

         A10: z <> [x, y] and

         A11: [ [x, y], z] in DOX;

        consider x9,y9 be object such that

         A12: z = [x9, y9] and

         A13: x9 in ( bool X) and

         A14: y9 in ( bool X) by A9, RELSET_1: 2;

        consider e,f be Dependency of X such that

         A15: [ [x, y], z] = [e, f] and

         A16: e <= f by A11;

        

         A17: e = [x, y] by A15, XTUPLE_0: 1;

        

         A18: f = z by A15, XTUPLE_0: 1;

        reconsider x9, y9 as Subset of X by A13, A14;

        x <> x9 or y <> y9 by A10, A12;

        hence contradiction by A8, A9, A12, A13, A14, A16, A17, A18;

      end;

      then [x, y] in ( Maximal_wrt F) by Def1;

      hence thesis;

    end;

    definition

      let X be set, M be Dependency-set of X;

      :: ARMSTRNG:def18

      attr M is (M1) means for A be Subset of X holds ex A9,B9 be Subset of X st [A9, B9] >= [A, A] & [A9, B9] in M;

      :: ARMSTRNG:def19

      attr M is (M2) means for A,B,A9,B9 be Subset of X st [A, B] in M & [A9, B9] in M & [A, B] >= [A9, B9] holds A = A9 & B = B9;

      :: ARMSTRNG:def20

      attr M is (M3) means for A,B,A9,B9 be Subset of X st [A, B] in M & [A9, B9] in M & A9 c= B holds B9 c= B;

    end

    theorem :: ARMSTRNG:28

    

     Th28: for X be finite non empty set, F be Full-family of X holds ( Maximal_wrt F) is (M1) (M2) (M3)

    proof

      let X be finite non empty set, F be full_family Dependency-set of X;

      set DOX = ( Dependencies-Order X);

      set MEF = ( Maximal_wrt F);

      thus ( Maximal_wrt F) is (M1)

      proof

        

         A1: ( field DOX) = [:( bool X), ( bool X):] by Th17;

        let A be Subset of X;

        defpred P[ object] means ex y be Dependency of X st $1 = y & y >= [A, A];

        consider MA be set such that

         A2: for x be object holds x in MA iff x in F & P[x] from XBOOLE_0:sch 1;

        MA c= F by A2;

        then

         A3: MA is finite Subset of ( field DOX) by A1, XBOOLE_1: 1;

         [A, A] in F by Def15;

        then MA <> {} by A2;

        then

        consider x be Element of MA such that

         A4: x is_maximal_wrt (MA,DOX) by A3, Th2;

        

         A5: x in MA by A4;

        then x in F by A2;

        then

        consider A9,B9 be object such that

         A6: A9 in ( bool X) and

         A7: B9 in ( bool X) and

         A8: x = [A9, B9] by ZFMISC_1:def 2;

        reconsider A9, B9 as Subset of X by A6, A7;

        take A9, B9;

        

         A9: ex y be Dependency of X st x = y & y >= [A, A] by A2, A5;

        hence [A9, B9] >= [A, A] by A8;

        x is_maximal_wrt (F,DOX)

        proof

          thus x in F by A2, A5;

          given z be set such that

           A10: z in F and

           A11: z <> x and

           A12: [x, z] in DOX;

          consider e,f be Dependency of X such that

           A13: [x, z] = [e, f] and

           A14: e <= f by A12;

          x = e by A13, XTUPLE_0: 1;

          then

           A15: f >= [A, A] by A9, A14, Th12;

          z = f by A13, XTUPLE_0: 1;

          then z in MA by A2, A10, A15;

          hence contradiction by A4, A11, A12;

        end;

        hence thesis by A8, Def1;

      end;

      thus ( Maximal_wrt F) is (M2)

      proof

        let A,B,A9,B9 be Subset of X such that

         A16: [A, B] in MEF and

         A17: [A9, B9] in MEF and

         A18: [A, B] >= [A9, B9];

        

         A19: [ [A9, B9], [A, B]] in DOX by A18;

        assume not (A = A9 & B = B9);

        then

         A20: [A, B] <> [A9, B9] by XTUPLE_0: 1;

         [A9, B9] is_maximal_wrt (F,DOX) by A17, Def1;

        hence contradiction by A16, A20, A19;

      end;

      thus ( Maximal_wrt F) is (M3)

      proof

        let A,B,A9,B9 be Subset of X;

        assume that

         A21: [A, B] in MEF and

         A22: [A9, B9] in MEF and

         A23: A9 c= B;

        

         A24: A ^|^ (B,F) by A21;

         [A9, B9] >= [B, B9] by A23;

        then [B, B9] in F by A22, Def12;

        then

         A25: [A, B9] in F by A21, Th18;

        B c= (B \/ B9) by XBOOLE_1: 7;

        then

         A26: [A, (B \/ B9)] >= [A, B];

        (A \/ A) = A;

        then [A, (B \/ B9)] in F by A21, A25, Def13;

        then (B \/ B9) = B by A24, A26, Th27;

        hence thesis by XBOOLE_1: 11;

      end;

    end;

    theorem :: ARMSTRNG:29

    

     Th29: for X be finite set, M,F be Dependency-set of X st M is (M1) (M2) (M3) & F = { [A, B] where A,B be Subset of X : ex A9,B9 be Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M } holds M = ( Maximal_wrt F) & F is full_family & for G be Full-family of X st M = ( Maximal_wrt G) holds G = F

    proof

      let X be finite set, M be Dependency-set of X, F be Dependency-set of X;

      assume that

       A1: M is (M1) (M2) (M3) and

       A2: F = { [A, B] where A,B be Subset of X : ex A9,B9 be Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M };

      

       A3: F is (F1)

      proof

        let A be Subset of X;

        ex A9,B9 be Subset of X st [A9, B9] >= [A, A] & [A9, B9] in M by A1;

        hence thesis by A2;

      end;

       A4:

      now

        let x be set;

        assume x in F;

        then

        consider a,b be Subset of X such that

         A5: x = [a, b] and

         A6: ex a9,b9 be Subset of X st [a9, b9] >= [a, b] & [a9, b9] in M by A2;

        consider a9,b9 be Subset of X such that

         A7: [a9, b9] >= [a, b] and

         A8: [a9, b9] in M by A6;

        take a, b, a9, b9;

        thus x = [a, b] & [a9, b9] >= [a, b] & [a9, b9] in M by A5, A7, A8;

      end;

       A9:

      now

        let A,B be Subset of X;

        assume [A, B] in F;

        then

        consider a,b,a9,b9 be Subset of X such that

         A10: [A, B] = [a, b] and

         A11: [a9, b9] >= [a, b] and

         A12: [a9, b9] in M by A4;

        take a9, b9;

        thus [a9, b9] >= [A, B] & [a9, b9] in M by A10, A11, A12;

      end;

      now

        let A,B,C be Subset of X;

        assume that

         A13: [A, B] in F and

         A14: [B, C] in F;

        consider A9,B9 be Subset of X such that

         A15: [A9, B9] >= [A, B] and

         A16: [A9, B9] in M by A9, A13;

        consider B19,C9 be Subset of X such that

         A17: [B19, C9] >= [B, C] and

         A18: [B19, C9] in M by A9, A14;

        

         A19: B19 c= B by A17;

        B c= B9 by A15;

        then B19 c= B9 by A19;

        then C9 c= B9 by A1, A16, A18;

        then

         A20: [A9, B9] >= [A9, C9];

        

         A21: C c= C9 by A17;

        A9 c= A by A15;

        then [A9, C9] >= [A, C] by A21;

        then [A9, B9] >= [A, C] by A20, Th12;

        hence [A, C] in F by A2, A16;

      end;

      then

       A22: F is (F2) by Th18;

      

       A23: F is (F4)

      proof

        let A,B,A9,B9 be Subset of X such that

         A24: [A, B] in F and

         A25: [A9, B9] in F;

        consider a1,b1 be Subset of X such that

         A26: [a1, b1] >= [A, B] and

         A27: [a1, b1] in M by A9, A24;

        

         A28: B c= b1 by A26;

        consider a19,b19 be Subset of X such that

         A29: [a19, b19] >= [A9, B9] and

         A30: [a19, b19] in M by A9, A25;

        

         A31: B9 c= b19 by A29;

        consider A99,B99 be Subset of X such that

         A32: [A99, B99] >= [(A \/ A9), (A \/ A9)] and

         A33: [A99, B99] in M by A1;

        

         A34: (A \/ A9) c= B99 by A32;

        a19 c= A9 by A29;

        then a19 c= (A \/ A9) by XBOOLE_1: 10;

        then a19 c= B99 by A34;

        then b19 c= B99 by A1, A33, A30;

        then

         A35: B9 c= B99 by A31;

        a1 c= A by A26;

        then a1 c= (A \/ A9) by XBOOLE_1: 10;

        then a1 c= B99 by A34;

        then b1 c= B99 by A1, A33, A27;

        then B c= B99 by A28;

        then

         A36: (B \/ B9) c= (B99 \/ B99) by A35, XBOOLE_1: 13;

        A99 c= (A \/ A9) by A32;

        then [A99, B99] >= [(A \/ A9), (B \/ B9)] by A36;

        hence thesis by A2, A33;

      end;

      set DOX = ( Dependencies-Order X);

      now

        let x be object;

        hereby

          assume

           A37: x in M;

          then

          consider a,b be Subset of X such that

           A38: x = [a, b] by Th9;

          x is_maximal_wrt (F,DOX)

          proof

            thus x in F by A2, A37, A38;

            given y be set such that

             A39: y in F and

             A40: y <> x and

             A41: [x, y] in DOX;

            consider e,f be Dependency of X such that

             A42: [x, y] = [e, f] and

             A43: e <= f by A41;

            

             A44: y = f by A42, XTUPLE_0: 1;

            consider c,d,c9,d9 be Subset of X such that

             A45: y = [c, d] and

             A46: [c9, d9] >= [c, d] and

             A47: [c9, d9] in M by A4, A39;

            

             A48: x = e by A42, XTUPLE_0: 1;

            then

             A49: [c9, d9] >= [a, b] by A38, A43, A44, A45, A46, Th12;

            then

             A50: d9 = b by A1, A37, A38, A47;

            c9 = a by A1, A37, A38, A47, A49;

            hence contradiction by A38, A40, A43, A48, A44, A45, A46, A50, Th11;

          end;

          hence x in ( Maximal_wrt F) by Def1;

        end;

        assume

         A51: x in ( Maximal_wrt F);

        then

         A52: x is_maximal_wrt (F,DOX) by Def1;

        assume

         A53: not x in M;

        consider a,b,a9,b9 be Subset of X such that

         A54: x = [a, b] and

         A55: [a9, b9] >= [a, b] and

         A56: [a9, b9] in M by A4, A51;

        

         A57: [ [a, b], [a9, b9]] in DOX by A55;

         [a9, b9] in F by A2, A56;

        hence contradiction by A52, A54, A56, A53, A57;

      end;

      hence M = ( Maximal_wrt F) by TARSKI: 2;

      F is (F3)

      proof

        let A,B,A9,B9 be Subset of X such that

         A58: [A, B] in F and

         A59: [A, B] >= [A9, B9];

        consider a9,b9 be Subset of X such that

         A60: [a9, b9] >= [A, B] and

         A61: [a9, b9] in M by A9, A58;

         [a9, b9] >= [A9, B9] by A59, A60, Th12;

        hence thesis by A2, A61;

      end;

      hence F is full_family by A3, A22, A23;

      let G be Full-family of X such that

       A62: M = ( Maximal_wrt G);

      now

        let x be object;

        hereby

          

           A63: ( field DOX) = [:( bool X), ( bool X):] by Th17;

          assume

           A64: x in G;

          then

          consider a,b be Subset of X such that

           A65: x = [a, b] by Th9;

          defpred P[ object] means ex y be Dependency of X st $1 = y & y >= [a, b];

          consider MA be set such that

           A66: for x be object holds x in MA iff x in G & P[x] from XBOOLE_0:sch 1;

          MA c= G by A66;

          then

           A67: MA is finite Subset of ( field DOX) by A63, XBOOLE_1: 1;

          MA <> {} by A64, A65, A66;

          then

          consider m be Element of MA such that

           A68: m is_maximal_wrt (MA,DOX) by A67, Th2;

          

           A69: m in MA by A68;

          then m in G by A66;

          then

           A70: ex a9,b9 be Subset of X st m = [a9, b9] by Th9;

          m is_maximal_wrt (G,DOX)

          proof

            

             A71: ex mm be Dependency of X st m = mm & mm >= [a, b] by A66, A69;

            thus m in G by A66, A69;

            given y be set such that

             A72: y in G and

             A73: y <> m and

             A74: [m, y] in DOX;

            consider e,f be Dependency of X such that

             A75: [m, y] = [e, f] and

             A76: e <= f by A74;

            

             A77: y = f by A75, XTUPLE_0: 1;

            m = e by A75, XTUPLE_0: 1;

            then f >= [a, b] by A71, A76, Th12;

            then y in MA by A66, A72, A77;

            hence contradiction by A68, A73, A74;

          end;

          then

           A78: m in (DOX Maximal_in G) by Def1;

          ex y be Dependency of X st m = y & y >= [a, b] by A66, A69;

          hence x in F by A2, A62, A65, A78, A70;

        end;

        assume x in F;

        then ex a,b,a1,b1 be Subset of X st x = [a, b] & [a1, b1] >= [a, b] & [a1, b1] in M by A4;

        hence x in G by A62, Def12;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let X be non empty finite set, F be Full-family of X;

      cluster ( Maximal_wrt F) -> non empty;

      coherence

      proof

        set M = ( Maximal_wrt F);

        M is (M1) by Th28;

        then ex A9,B9 be Subset of X st [A9, B9] >= [( [#] X), ( [#] X)] & [A9, B9] in M;

        hence thesis;

      end;

    end

    theorem :: ARMSTRNG:30

    

     Th30: for X be finite set, F be Dependency-set of X, K be Subset of X st F = { [A, B] where A,B be Subset of X : K c= A or B c= A } holds ( { [K, X]} \/ { [A, A] where A be Subset of X : not K c= A }) = ( Maximal_wrt F)

    proof

      let X be finite set, F be Dependency-set of X, K be Subset of X;

      set M = ( { [K, X]} \/ { [A, A] where A be Subset of X : not K c= A });

      

       A1: { [K, X]} c= M by XBOOLE_1: 7;

       A2:

      now

        let A be Subset of X;

        assume not K c= A;

        then

         A3: [A, A] in { [a, a] where a be Subset of X : not K c= a };

        { [a, a] where a be Subset of X : not K c= a } c= M by XBOOLE_1: 7;

        hence [A, A] in M by A3;

      end;

      

       A4: ( [#] X) = X;

      

       A5: M c= [:( bool X), ( bool X):]

      proof

        let x be object;

        assume

         A6: x in M;

        per cases by A6, XBOOLE_0:def 3;

          suppose x in { [K, X]};

          then x = [K, X] by TARSKI:def 1;

          hence thesis by A4, ZFMISC_1:def 2;

        end;

          suppose x in { [A, A] where A be Subset of X : not K c= A };

          then ex A be Subset of X st x = [A, A] & not K c= A;

          hence thesis;

        end;

      end;

       A7:

      now

        let A,B be Subset of X;

        assume

         A8: [A, B] in M;

        per cases by A8, XBOOLE_0:def 3;

          suppose [A, B] in { [K, X]};

          hence [A, B] = [K, X] or not K c= A & A = B by TARSKI:def 1;

        end;

          suppose [A, B] in { [a, a] where a be Subset of X : not K c= a };

          then

          consider a be Subset of X such that

           A9: [A, B] = [a, a] and

           A10: not K c= a;

          A = a by A9, XTUPLE_0: 1;

          hence [A, B] = [K, X] or not K c= A & A = B by A9, A10, XTUPLE_0: 1;

        end;

      end;

      reconsider M as Dependency-set of X by A5;

      set FF = { [A, B] where A,B be Subset of X : ex A9,B9 be Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M };

      

       A11: FF c= [:( bool X), ( bool X):]

      proof

        let x be object;

        assume x in FF;

        then ex A,B be Subset of X st x = [A, B] & ex A9,B9 be Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M;

        hence thesis;

      end;

      

       A12: M is (M2)

      proof

        let A,B,A9,B9 be Subset of X such that

         A13: [A, B] in M and

         A14: [A9, B9] in M and

         A15: [A, B] >= [A9, B9];

        

         A16: A c= A9 by A15;

        

         A17: B9 c= B by A15;

        per cases by A7, A13;

          suppose

           A18: [A, B] = [K, X];

          thus A = A9 & B = B9

          proof

            per cases by A7, A14;

              suppose [A9, B9] = [K, X];

              hence thesis by A18, XTUPLE_0: 1;

            end;

              suppose not K c= A9 & A9 = B9;

              hence thesis by A16, A18, XTUPLE_0: 1;

            end;

          end;

        end;

          suppose

           A19: not K c= A & A = B;

          thus A = A9 & B = B9

          proof

            per cases by A7, A14;

              suppose [A9, B9] = [K, X];

              then B9 = X by XTUPLE_0: 1;

              then B = X by A17, XBOOLE_0:def 10;

              hence thesis by A19;

            end;

              suppose not K c= A9 & A9 = B9;

              hence thesis by A16, A17, A19, XBOOLE_0:def 10;

            end;

          end;

        end;

      end;

      reconsider FF as Dependency-set of X by A11;

      assume

       A20: F = { [A, B] where A,B be Subset of X : K c= A or B c= A };

       A21:

      now

        let x be object;

        hereby

          

           A22: { [a, a] where a be Subset of X : not K c= a } c= M by XBOOLE_1: 7;

          

           A23: [K, X] in { [K, X]} by TARSKI:def 1;

          

           A24: { [K, X]} c= M by XBOOLE_1: 7;

          assume x in F;

          then

          consider A,B be Subset of X such that

           A25: x = [A, B] and

           A26: K c= A or B c= A by A20;

          per cases ;

            suppose K c= A;

            then [K, ( [#] X)] >= [A, B];

            hence x in FF by A25, A24, A23;

          end;

            suppose

             A27: not K c= A;

            then

             A28: [A, A] in { [a, a] where a be Subset of X : not K c= a };

             [A, A] >= [A, B] by A26, A27;

            hence x in FF by A25, A22, A28;

          end;

        end;

        assume x in FF;

        then

        consider A,B be Subset of X such that

         A29: x = [A, B] and

         A30: ex A9,B9 be Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M;

        consider A9,B9 be Subset of X such that

         A31: [A9, B9] >= [A, B] and

         A32: [A9, B9] in M by A30;

        per cases by A32, XBOOLE_0:def 3;

          suppose [A9, B9] in { [K, X]};

          then [A9, B9] = [K, X] by TARSKI:def 1;

          then A9 = K by XTUPLE_0: 1;

          then K c= A by A31;

          hence x in F by A20, A29;

        end;

          suppose [A9, B9] in { [a, a] where a be Subset of X : not K c= a };

          then

          consider a be Subset of X such that

           A33: [A9, B9] = [a, a] and not K c= a;

          

           A34: A9 = a by A33, XTUPLE_0: 1;

          

           A35: B9 = a by A33, XTUPLE_0: 1;

          

           A36: B c= B9 by A31;

          A9 c= A by A31;

          then B c= A by A34, A35, A36;

          hence x in F by A20, A29;

        end;

      end;

      

       A37: M is (M3)

      proof

        let A,B,A9,B9 be Subset of X such that

         A38: [A, B] in M and

         A39: [A9, B9] in M and

         A40: A9 c= B;

        per cases by A7, A38;

          suppose [A, B] = [K, X];

          then B = X by XTUPLE_0: 1;

          hence thesis;

        end;

          suppose

           A41: not K c= A & A = B;

          thus B9 c= B

          proof

            per cases by A7, A39;

              suppose [A9, B9] = [K, X];

              hence thesis by A40, A41, XTUPLE_0: 1;

            end;

              suppose not K c= A9 & A9 = B9;

              hence thesis by A40;

            end;

          end;

        end;

      end;

      

       A42: [K, X] in { [K, X]} by TARSKI:def 1;

      M is (M1)

      proof

        let A be Subset of X;

        per cases ;

          suppose

           A43: K c= A;

          take A9 = K, B9 = ( [#] X);

          thus [A9, B9] >= [A, A] by A43;

          thus thesis by A42, A1;

        end;

          suppose

           A44: not K c= A;

          take A9 = A, B9 = A;

          thus [A9, B9] >= [A, A];

          thus thesis by A2, A44;

        end;

      end;

      then M = ( Maximal_wrt FF) by A12, A37, Th29;

      hence thesis by A21, TARSKI: 2;

    end;

    begin

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def21

      func saturated-subsets F -> Subset-Family of X equals { B where B be Subset of X : ex A be Subset of X st A ^|^ (B,F) };

      coherence

      proof

        set SS = { B where B be Subset of X : ex A be Subset of X st A ^|^ (B,F) };

        SS c= ( bool X)

        proof

          let x be object;

          assume x in SS;

          then ex B be Subset of X st x = B & ex A be Subset of X st A ^|^ (B,F);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    notation

      let X be set, F be Dependency-set of X;

      synonym closed_attribute_subset F for saturated-subsets F;

    end

    registration

      let X be set, F be finite Dependency-set of X;

      cluster ( saturated-subsets F) -> finite;

      coherence

      proof

        defpred P[ object, object] means ex a,b be object st $1 = [a, b] & $2 = ( [a, b] `2 );

        set ss = { B where B be Subset of X : ex A be Subset of X st A ^|^ (B,F) };

        

         A1: for x be object st x in F holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in F;

          then

          consider a,b be Subset of X such that

           A2: x = [a, b] by Th9;

          reconsider a, b as set;

          take b;

          take a, b;

          thus thesis by A2;

        end;

        consider f be Function such that

         A3: ( dom f) = F and

         A4: for x be object st x in F holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A5: ss c= ( rng f)

        proof

          let x be object;

          assume x in ss;

          then

          consider B be Subset of X such that

           A6: x = B and

           A7: ex A be Subset of X st A ^|^ (B,F);

          consider A be Subset of X such that

           A8: A ^|^ (B,F) by A7;

          

           A9: [A, B] in ( Maximal_wrt F) by A8;

          then

           A10: ex a,b be object st [A, B] = [a, b] & (f . [A, B]) = ( [a, b] `2 ) by A4;

          (f . [A, B]) = B by A10;

          hence thesis by A3, A6, A9, FUNCT_1: 3;

        end;

        ( rng f) is finite by A3, FINSET_1: 8;

        hence thesis by A5;

      end;

    end

    theorem :: ARMSTRNG:31

    

     Th31: for X,x be set, F be Dependency-set of X holds x in ( saturated-subsets F) iff ex B,A be Subset of X st x = B & A ^|^ (B,F)

    proof

      let X,x be set, F be Dependency-set of X;

      hereby

        assume x in ( saturated-subsets F);

        then

        consider B be Subset of X such that

         A1: x = B and

         A2: ex A be Subset of X st A ^|^ (B,F);

        consider A be Subset of X such that

         A3: A ^|^ (B,F) by A2;

        take B, A;

        thus x = B & A ^|^ (B,F) by A1, A3;

      end;

      given B,A be Subset of X such that

       A4: x = B and

       A5: A ^|^ (B,F);

      thus thesis by A4, A5;

    end;

    theorem :: ARMSTRNG:32

    

     Th32: for X be finite non empty set, F be Full-family of X holds ( saturated-subsets F) is (B1) (B2)

    proof

      let X be finite non empty set, F be Full-family of X;

      set ss = ( saturated-subsets F);

      

       A1: ( Maximal_wrt F) is (M1) by Th28;

      then

      consider A9,B9 be Subset of X such that

       A2: [A9, B9] >= [( [#] X), ( [#] X)] and

       A3: [A9, B9] in ( Maximal_wrt F);

      ( [#] X) c= B9 by A2;

      then

       A4: ( [#] X) = B9 by XBOOLE_0:def 10;

      A9 ^|^ (B9,F) by A3;

      then X in ss by A4;

      hence ss is (B1);

      thus ss is (B2)

      proof

        let a,b be set such that

         A5: a in ss and

         A6: b in ss;

        reconsider a9 = a, b9 = b as Subset of X by A5, A6;

        

         A7: ( Maximal_wrt F) is (M3) by Th28;

        consider B2,A2 be Subset of X such that

         A8: b = B2 and

         A9: A2 ^|^ (B2,F) by A6, Th31;

        

         A10: [A2, B2] in ( Maximal_wrt F) by A9;

        consider B1,A1 be Subset of X such that

         A11: a = B1 and

         A12: A1 ^|^ (B1,F) by A5, Th31;

        

         A13: [A1, B1] in ( Maximal_wrt F) by A12;

        consider A9,B9 be Subset of X such that

         A14: [A9, B9] >= [(a9 /\ b9), (a9 /\ b9)] and

         A15: [A9, B9] in ( Maximal_wrt F) by A1;

        

         A16: A9 c= (a /\ b) by A14;

        (a /\ b) c= b by XBOOLE_1: 17;

        then A9 c= B2 by A8, A16;

        then

         A17: B9 c= B2 by A10, A15, A7;

        

         A18: (a /\ b) c= B9 by A14;

        (a /\ b) c= a by XBOOLE_1: 17;

        then A9 c= B1 by A11, A16;

        then B9 c= B1 by A13, A15, A7;

        then B9 c= (a /\ b) by A11, A8, A17, XBOOLE_1: 19;

        then

         A19: B9 = (a /\ b) by A18, XBOOLE_0:def 10;

        A9 ^|^ (B9,F) by A15;

        hence thesis by A19;

      end;

    end;

    definition

      let X be set, B be set;

      :: ARMSTRNG:def22

      func X deps_encl_by B -> Dependency-set of X equals { [a, b] where a,b be Subset of X : for c be set st c in B & a c= c holds b c= c };

      coherence

      proof

        set F = { [a, b] where a,b be Subset of X : for c be set st c in B & a c= c holds b c= c };

        F c= [:( bool X), ( bool X):]

        proof

          let x be object;

          assume x in F;

          then ex a,b be Subset of X st x = [a, b] & for c be set st c in B & a c= c holds b c= c;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ARMSTRNG:33

    

     Th33: for X be set, B be Subset-Family of X, F be Dependency-set of X holds (X deps_encl_by B) is full_family

    proof

      let X be set, B be Subset-Family of X, F be Dependency-set of X;

      set F = (X deps_encl_by B);

      per cases ;

        suppose

         A1: B is empty;

        now

          let x be object;

          thus x in F implies x in ( Dependencies X);

          assume x in ( Dependencies X);

          then

          consider x1,x2 be object such that

           A2: x1 in ( bool X) and

           A3: x2 in ( bool X) and

           A4: x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1, x2 as set by TARSKI: 1;

          for g be set st g in B & x1 c= g holds x2 c= g by A1;

          hence x in F by A2, A3, A4;

        end;

        then F = ( Dependencies X) by TARSKI: 2;

        then F is (F1) (F2) (F3) (F4) by Th19;

        hence thesis;

      end;

        suppose B is non empty;

        then

        reconsider B as non empty Subset-Family of X;

        thus F is (F1)

        proof

          let A be Subset of X;

          for c be set st c in B & A c= c holds A c= c;

          hence thesis;

        end;

         A5:

        now

          let x,y be Subset of X, c be Element of B;

          assume that

           A6: [x, y] in F and

           A7: x c= c;

          consider a,b be Subset of X such that

           A8: [x, y] = [a, b] and

           A9: for c be set st c in B & a c= c holds b c= c by A6;

          

           A10: y = b by A8, XTUPLE_0: 1;

          x = a by A8, XTUPLE_0: 1;

          hence y c= c by A7, A9, A10;

        end;

        now

          let a,b,c be Subset of X such that

           A11: [a, b] in F and

           A12: [b, c] in F;

          now

            let x be set;

            assume that

             A13: x in B and

             A14: a c= x;

            b c= x by A5, A11, A13, A14;

            hence c c= x by A5, A12, A13;

          end;

          hence [a, c] in F;

        end;

        hence F is (F2) by Th18;

        thus F is (F3)

        proof

          let a,b,a9,b9 be Subset of X such that

           A15: [a, b] in F and

           A16: [a, b] >= [a9, b9];

          

           A17: b9 c= b by A16;

          

           A18: a c= a9 by A16;

          now

            let c be set;

            assume that

             A19: c in B and

             A20: a9 c= c;

            a c= c by A18, A20;

            then b c= c by A5, A15, A19;

            hence b9 c= c by A17;

          end;

          hence thesis;

        end;

        thus F is (F4)

        proof

          let a,b,a9,b9 be Subset of X such that

           A21: [a, b] in F and

           A22: [a9, b9] in F;

          now

            let c be set;

            assume that

             A23: c in B and

             A24: (a \/ a9) c= c;

            a9 c= c by A24, XBOOLE_1: 11;

            then

             A25: b9 c= c by A5, A22, A23;

            a c= c by A24, XBOOLE_1: 11;

            then b c= c by A5, A21, A23;

            hence (b \/ b9) c= c by A25, XBOOLE_1: 8;

          end;

          hence thesis;

        end;

      end;

    end;

    theorem :: ARMSTRNG:34

    

     Th34: for X be finite non empty set, B be Subset-Family of X holds B c= ( saturated-subsets (X deps_encl_by B))

    proof

      let X be finite non empty set, B be Subset-Family of X;

      set F = (X deps_encl_by B);

      reconsider F9 = F as Full-family of X by Th33;

      set M = ( Maximal_wrt F9);

      let x be object;

      assume

       A1: x in B;

      then

      reconsider x9 = x as Element of B;

      reconsider x99 = x as Subset of X by A1;

      M is (M1) by Th28;

      then

      consider a9,b9 be Subset of X such that

       A2: [a9, b9] >= [x99, x99] and

       A3: [a9, b9] in M;

      

       A4: a9 c= x99 by A2;

       [a9, b9] in F by A3;

      then

      consider a,b be Subset of X such that

       A5: [a9, b9] = [a, b] and

       A6: for c be set st c in B & a c= c holds b c= c;

      

       A7: a ^|^ (b,F) by A3, A5;

      a9 = a by A5, XTUPLE_0: 1;

      then

       A8: b c= x9 by A1, A4, A6;

      

       A9: b9 = b by A5, XTUPLE_0: 1;

      x99 c= b9 by A2;

      then b = x by A9, A8, XBOOLE_0:def 10;

      hence thesis by A7;

    end;

    theorem :: ARMSTRNG:35

    

     Th35: for X be finite non empty set, B be Subset-Family of X st B is (B1) (B2) holds B = ( saturated-subsets (X deps_encl_by B)) & for G be Full-family of X st B = ( saturated-subsets G) holds G = (X deps_encl_by B)

    proof

      let X be finite non empty set, B be Subset-Family of X;

      set F = (X deps_encl_by B);

      reconsider F9 = F as Full-family of X by Th33;

      set ss = ( saturated-subsets F);

      set M = ( Maximal_wrt F9);

      assume

       A1: B is (B1) (B2);

      then

      reconsider B9 = B as non empty set;

      

       A2: X in B by A1;

      now

        let x be object;

        B c= ss by Th34;

        hence x in B implies x in ss;

        assume x in ss;

        then

        consider b,a be Subset of X such that

         A3: x = b and

         A4: a ^|^ (b,F) by Th31;

         [a, b] in M by A4;

        then [a, b] in F;

        then

        consider aa,bb be Subset of X such that

         A5: [a, b] = [aa, bb] and

         A6: for c be set st c in B & aa c= c holds bb c= c;

        

         A7: b = bb by A5, XTUPLE_0: 1;

        set S = { b9 where b9 be Element of B9 : a c= b9 };

        

         A8: S c= ( bool X)

        proof

          let x be object;

          assume x in S;

          then

          consider b9 be Element of B9 such that

           A9: x = b9 and a c= b9;

          b9 in B9;

          hence thesis by A9;

        end;

        

         A10: S c= B

        proof

          let x be object;

          assume x in S;

          then ex b9 be Element of B9 st x = b9 & a c= b9;

          hence thesis;

        end;

        

         A11: X in S by A2;

        reconsider S as Subset-Family of X by A8;

        set mS = ( Intersect S);

        reconsider mS as Subset of X;

        

         A12: a = aa by A5, XTUPLE_0: 1;

        

         A13: b c= mS

        proof

          let x be object;

          assume

           A14: x in b;

          now

            let Y be set;

            assume Y in S;

            then

            consider b9 be Element of B9 such that

             A15: Y = b9 and

             A16: a c= b9;

            b c= b9 by A6, A12, A7, A16;

            hence x in Y by A14, A15;

          end;

          then x in ( meet S) by A11, SETFAM_1:def 1;

          hence thesis by A11, SETFAM_1:def 9;

        end;

        now

          now

            let c be set;

            assume that

             A17: c in B and

             A18: a c= c;

            c in S by A17, A18;

            then ( meet S) c= c by SETFAM_1: 3;

            hence mS c= c by A11, SETFAM_1:def 9;

          end;

          then

           A19: [a, mS] in F;

          assume

           A20: b <> mS;

           [a, mS] >= [a, b] by A13;

          hence contradiction by A4, A20, A19, Th27;

        end;

        hence x in B by A1, A3, A10, Th1;

      end;

      hence B = ( saturated-subsets F) by TARSKI: 2;

      let G be Full-family of X;

      assume

       A21: B = ( saturated-subsets G);

      set MG = ( Maximal_wrt G);

      

       A22: MG is (M1) (M3) by Th28;

      now

        let x be object;

        hereby

          assume x in G;

          then

          reconsider x1 = x as Element of G;

          reconsider x9 = x1 as Dependency of X;

          consider a,b be Subset of X such that

           A23: x9 = [a, b] by Th8;

          now

            consider a99,b99 be Subset of X such that

             A24: [a99, b99] in MG and

             A25: [a99, b99] >= x9 by Th26;

            

             A26: b c= b99 by A23, A25;

            let b9 be set such that

             A27: b9 in B9 and

             A28: a c= b9;

            consider b19,a9 be Subset of X such that

             A29: b9 = b19 and

             A30: a9 ^|^ (b19,G) by A21, A27, Th31;

            a99 c= a by A23, A25;

            then

             A31: a99 c= b9 by A28;

             [a9, b9] in MG by A29, A30;

            then b99 c= b19 by A22, A29, A24, A31;

            hence b c= b9 by A29, A26;

          end;

          hence x in F by A23;

        end;

        assume x in F;

        then

        consider a,b be Subset of X such that

         A32: x = [a, b] and

         A33: for c be set st c in B & a c= c holds b c= c;

        consider a9,b9 be Subset of X such that

         A34: [a9, b9] >= [a, a] and

         A35: [a9, b9] in MG by A22;

        

         A36: a9 c= a by A34;

        a9 ^|^ (b9,G) by A35;

        then

         A37: b9 in B by A21;

        a c= b9 by A34;

        then b c= b9 by A33, A37;

        then [a9, b9] >= [a, b] by A36;

        hence x in G by A32, A35, Def12;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def23

      func enclosure_of F -> Subset-Family of X equals { b where b be Subset of X : for A,B be Subset of X st [A, B] in F & A c= b holds B c= b };

      coherence

      proof

        set B = { b where b be Subset of X : for x,y be Subset of X st [x, y] in F & x c= b holds y c= b };

        B c= ( bool X)

        proof

          let z be object;

          assume z in B;

          then ex b be Subset of X st z = b & for x,y be Subset of X st [x, y] in F & x c= b holds y c= b;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ARMSTRNG:36

    

     Th36: for X be finite non empty set, F be Dependency-set of X holds ( enclosure_of F) is (B1) (B2)

    proof

      let X be finite non empty set, F be Dependency-set of X;

      set B = ( enclosure_of F);

      

       A1: for x,y be Subset of X st [x, y] in F & x c= X holds y c= X;

      X = ( [#] X);

      then X in B by A1;

      hence B is (B1);

      let a,b be set such that

       A2: a in B and

       A3: b in B;

      consider b9 be Subset of X such that

       A4: b9 = b and

       A5: for x,y be Subset of X st [x, y] in F & x c= b9 holds y c= b9 by A3;

      consider a9 be Subset of X such that

       A6: a9 = a and

       A7: for x,y be Subset of X st [x, y] in F & x c= a9 holds y c= a9 by A2;

      reconsider ab = (a9 /\ b9) as Subset of X;

      now

        let x,y be Subset of X such that

         A8: [x, y] in F and

         A9: x c= ab;

        

         A10: y c= b9 by A5, A8, A9, XBOOLE_1: 18;

        y c= a9 by A7, A8, A9, XBOOLE_1: 18;

        hence y c= ab by A10, XBOOLE_1: 19;

      end;

      hence thesis by A6, A4;

    end;

    theorem :: ARMSTRNG:37

    

     Th37: for X be finite non empty set, F be Dependency-set of X holds F c= (X deps_encl_by ( enclosure_of F)) & for G be Dependency-set of X st F c= G & G is full_family holds (X deps_encl_by ( enclosure_of F)) c= G

    proof

      let X be finite non empty set, F be Dependency-set of X;

      set B = ( enclosure_of F);

      set H = (X deps_encl_by B);

      thus F c= H

      proof

        let x be object;

        assume

         A1: x in F;

        then

        consider a,b be Subset of X such that

         A2: x = [a, b] by Th9;

        now

          let c be set such that

           A3: c in B and

           A4: a c= c and

           A5: not b c= c;

          reconsider c as Subset of X by A3;

          ex c9 be Subset of X st c9 = c & for x,y be Subset of X st [x, y] in F & x c= c9 holds y c= c9 by A3;

          hence contradiction by A1, A2, A4, A5;

        end;

        hence thesis by A2;

      end;

      let G be Dependency-set of X such that

       A6: F c= G and

       A7: G is full_family;

      set B9 = ( saturated-subsets G);

      let z be object;

      set GG = { [e, f] where e,f be Subset of X : for c be set st c in B9 & e c= c holds f c= c };

      

       A8: GG = (X deps_encl_by B9);

      B is (B1) (B2) by Th36;

      then

       A9: B = ( saturated-subsets H) by Th35;

      assume z in H;

      then

      consider a,b be Subset of X such that

       A10: z = [a, b] and

       A11: for c be set st c in B & a c= c holds b c= c;

      B9 is (B1) (B2) by A7, Th32;

      then

       A12: GG = G by A7, A8, Th35;

      B9 c= ( saturated-subsets H)

      proof

        let d be object such that

         A13: d in B9 and

         A14: not d in ( saturated-subsets H);

        reconsider d as Subset of X by A13;

        consider x,y be Subset of X such that

         A15: [x, y] in F and

         A16: x c= d and

         A17: not y c= d by A9, A14;

         [x, y] in G by A6, A15;

        then

        consider e,f be Subset of X such that

         A18: [x, y] = [e, f] and

         A19: for c be set st c in B9 & e c= c holds f c= c by A12;

        

         A20: y = f by A18, XTUPLE_0: 1;

        x = e by A18, XTUPLE_0: 1;

        hence contradiction by A13, A16, A17, A19, A20;

      end;

      then for c be set st c in B9 & a c= c holds b c= c by A11, A9;

      hence thesis by A10, A12;

    end;

    definition

      let X be finite non empty set, F be Dependency-set of X;

      :: ARMSTRNG:def24

      func Dependency-closure F -> Full-family of X means

      : Def24: F c= it & for G be Dependency-set of X st F c= G & G is full_family holds it c= G;

      existence

      proof

        set B = { c where c be Subset of X : for x,y be Subset of X st [x, y] in F & x c= c holds y c= c };

        

         A1: B = ( enclosure_of F);

        B c= ( bool X)

        proof

          let x be object;

          assume x in B;

          then ex c be Subset of X st x = c & for x,y be Subset of X st [x, y] in F & x c= c holds y c= c;

          hence thesis;

        end;

        then

        reconsider B as Subset-Family of X;

        set H = (X deps_encl_by B);

        reconsider H as Full-family of X by Th33;

        take H;

        thus thesis by A1, Th37;

      end;

      correctness

      proof

        let it1,it2 be Full-family of X;

        assume that

         A2: F c= it1 and

         A3: for G be Dependency-set of X st F c= G & G is full_family holds it1 c= G and

         A4: F c= it2 and

         A5: for G be Dependency-set of X st F c= G & G is full_family holds it2 c= G;

        

         A6: it2 c= it1 by A2, A5;

        it1 c= it2 by A3, A4;

        hence it1 = it2 by A6, XBOOLE_0:def 10;

      end;

    end

    theorem :: ARMSTRNG:38

    

     Th38: for X be finite non empty set, F be Dependency-set of X holds ( Dependency-closure F) = (X deps_encl_by ( enclosure_of F))

    proof

      let X be finite non empty set, F be Dependency-set of X;

      set B = ( enclosure_of F);

      set H = (X deps_encl_by B);

      reconsider H as Full-family of X by Th33;

      

       A1: for G be Dependency-set of X st F c= G & G is full_family holds H c= G by Th37;

      F c= H by Th37;

      hence thesis by A1, Def24;

    end;

    theorem :: ARMSTRNG:39

    

     Th39: for X be set, K be Subset of X, B be Subset-Family of X st B = ( {X} \/ { A where A be Subset of X : not K c= A }) holds B is (B1) (B2)

    proof

      let X be set, K be Subset of X, BB be Subset-Family of X such that

       A1: BB = ( {X} \/ { B where B be Subset of X : not K c= B });

      X in {X} by TARSKI:def 1;

      then X in BB by A1, XBOOLE_0:def 3;

      hence BB is (B1);

      set BB1 = { B where B be Subset of X : not K c= B };

      thus BB is (B2)

      proof

        let a,b be set;

        assume that

         A2: a in BB and

         A3: b in BB;

        reconsider a9 = a, b9 = b as Subset of X by A2, A3;

        per cases by A1, A2, A3, XBOOLE_0:def 3;

          suppose

           A4: a in {X} & b in {X};

          then

           A5: b = X by TARSKI:def 1;

          a = X by A4, TARSKI:def 1;

          then (a /\ b) in {X} by A5, TARSKI:def 1;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

          suppose

           A6: a in {X} & b in BB1;

          then a = X by TARSKI:def 1;

          then (a9 /\ b9) = b by XBOOLE_1: 28;

          hence thesis by A1, A6, XBOOLE_0:def 3;

        end;

          suppose

           A7: a in BB1 & b in {X};

          then b = X by TARSKI:def 1;

          then (a9 /\ b9) = a by XBOOLE_1: 28;

          hence thesis by A1, A7, XBOOLE_0:def 3;

        end;

          suppose a in BB1 & b in BB1;

          then ex B1 be Subset of X st b = B1 & not K c= B1;

          then not K c= (a /\ b) by XBOOLE_1: 18;

          then (a9 /\ b9) in BB1;

          hence thesis by A1, XBOOLE_0:def 3;

        end;

      end;

    end;

    theorem :: ARMSTRNG:40

    for X be finite non empty set, F be Dependency-set of X, K be Subset of X st F = { [A, B] where A,B be Subset of X : K c= A or B c= A } holds ( {X} \/ { B where B be Subset of X : not K c= B }) = ( saturated-subsets F)

    proof

      let X be finite non empty set, F be Dependency-set of X, K be Subset of X;

      set BB = ( {X} \/ { B where B be Subset of X : not K c= B });

      BB c= ( bool X)

      proof

        let x be object;

        assume

         A1: x in BB;

        per cases by A1, XBOOLE_0:def 3;

          suppose

           A2: x in {X};

           {X} c= ( bool X) by ZFMISC_1: 68;

          hence thesis by A2;

        end;

          suppose x in { B where B be Subset of X : not K c= B };

          then ex B be Subset of X st x = B & not K c= B;

          hence thesis;

        end;

      end;

      then

      reconsider BB9 = BB as non empty Subset-Family of X;

      set G = { [a, b] where a,b be Subset of X : for c be set st c in BB9 & a c= c holds b c= c };

      

       A3: G = (X deps_encl_by BB9);

      

       A4: BB9 is (B2) by Th39;

      assume

       A5: F = { [A, B] where A,B be Subset of X : K c= A or B c= A };

      now

        let x be object;

        hereby

          assume x in F;

          then

          consider a,b be Subset of X such that

           A6: x = [a, b] and

           A7: K c= a or b c= a by A5;

          now

            let c be set such that

             A8: c in BB9 and

             A9: a c= c;

            per cases by A7;

              suppose

               A10: K c= a;

              thus b c= c

              proof

                per cases by A8, XBOOLE_0:def 3;

                  suppose c in {X};

                  then c = X by TARSKI:def 1;

                  hence thesis;

                end;

                  suppose c in { B where B be Subset of X : not K c= B };

                  then ex B be Subset of X st c = B & not K c= B;

                  hence thesis by A9, A10;

                end;

              end;

            end;

              suppose b c= a;

              hence b c= c by A9;

            end;

          end;

          hence x in G by A6;

        end;

        assume x in G;

        then

        consider a,b be Subset of X such that

         A11: x = [a, b] and

         A12: for c be set st c in BB9 & a c= c holds b c= c;

        now

          assume not K c= a;

          then a in { B where B be Subset of X : not K c= B };

          then a in BB9 by XBOOLE_0:def 3;

          hence b c= a by A12;

        end;

        hence x in F by A5, A11;

      end;

      then

       A13: F = G by TARSKI: 2;

      BB9 is (B1) by Th39;

      hence thesis by A4, A3, A13, Th35;

    end;

    theorem :: ARMSTRNG:41

    for X be finite set, F be Dependency-set of X, K be Subset of X st F = { [A, B] where A,B be Subset of X : K c= A or B c= A } holds ( {X} \/ { B where B be Subset of X : not K c= B }) = ( saturated-subsets F)

    proof

      let X be finite set, F be Dependency-set of X, K be Subset of X;

      set BB = ( {X} \/ { B where B be Subset of X : not K c= B });

      set M = ( { [K, X]} \/ { [A, A] where A be Subset of X : not K c= A });

      set ss = ( saturated-subsets F);

      assume F = { [A, B] where A,B be Subset of X : K c= A or B c= A };

      then

       A1: M = ( Maximal_wrt F) by Th30;

      

       A2: ( [#] X) = X;

      now

        let x be object;

        hereby

          assume

           A3: x in BB;

          per cases by A3, XBOOLE_0:def 3;

            suppose

             A4: x in {X};

             [K, X] in { [K, X]} by TARSKI:def 1;

            then [K, X] in M by XBOOLE_0:def 3;

            then

             A5: K ^|^ (X,F) by A1;

            x = X by A4, TARSKI:def 1;

            hence x in ss by A2, A5;

          end;

            suppose x in { B where B be Subset of X : not K c= B };

            then

            consider B be Subset of X such that

             A6: x = B and

             A7: not K c= B;

             [B, B] in { [A, A] where A be Subset of X : not K c= A } by A7;

            then [B, B] in M by XBOOLE_0:def 3;

            then B ^|^ (B,F) by A1;

            hence x in ss by A6;

          end;

        end;

        assume x in ss;

        then

        consider b,a be Subset of X such that

         A8: x = b and

         A9: a ^|^ (b,F) by Th31;

        

         A10: [a, b] in M by A1, A9;

        per cases by A10, XBOOLE_0:def 3;

          suppose [a, b] in { [K, X]};

          then [a, b] = [K, X] by TARSKI:def 1;

          then b = X by XTUPLE_0: 1;

          then b in {X} by TARSKI:def 1;

          hence x in BB by A8, XBOOLE_0:def 3;

        end;

          suppose [a, b] in { [A, A] where A be Subset of X : not K c= A };

          then

          consider c be Subset of X such that

           A11: [a, b] = [c, c] and

           A12: not K c= c;

          

           A13: c in { B where B be Subset of X : not K c= B } by A12;

          b = c by A11, XTUPLE_0: 1;

          hence x in BB by A8, A13, XBOOLE_0:def 3;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let X,G be set, B be Subset-Family of X;

      :: ARMSTRNG:def25

      pred G is_generator-set_of B means G c= B & B = { ( Intersect S) where S be Subset-Family of X : S c= G };

    end

    theorem :: ARMSTRNG:42

    for X be finite non empty set, G be Subset-Family of X holds G is_generator-set_of ( saturated-subsets (X deps_encl_by G))

    proof

      let X be finite non empty set, G be Subset-Family of X;

      set F = (X deps_encl_by G);

      set ssF = ( saturated-subsets F);

      F is full_family by Th33;

      then

       A1: ssF is (B1) (B2) by Th32;

      thus G is_generator-set_of ssF

      proof

        set H = { ( Intersect S) where S be Subset-Family of X : S c= G };

        thus

         A2: G c= ssF by Th34;

        now

          let x be object;

          hereby

            assume x in ssF;

            then

            consider b9,a9 be Subset of X such that

             A3: x = b9 and

             A4: a9 ^|^ (b9,F) by Th31;

             [a9, b9] in ( Maximal_wrt F) by A4;

            then [a9, b9] in F;

            then

            consider a,b be Subset of X such that

             A5: [a, b] = [a9, b9] and

             A6: for c be set st c in G & a c= c holds b c= c;

            set C = { c where c be Subset of X : c in G & a c= c };

            C c= ( bool X)

            proof

              let x be object;

              assume x in C;

              then ex c be Subset of X st x = c & c in G & a c= c;

              hence thesis;

            end;

            then

            reconsider C as Subset-Family of X;

            now

              let z1 be set;

              assume z1 in C;

              then ex c be Subset of X st z1 = c & c in G & a c= c;

              hence b c= z1 by A6;

            end;

            then

             A7: b c= ( Intersect C) by MSSUBFAM: 4;

            set ic = ( Intersect C);

            

             A8: b = b9 by A5, XTUPLE_0: 1;

            

             A9: C c= G

            proof

              let c be object;

              assume c in C;

              then ex cc be Subset of X st cc = c & cc in G & a c= cc;

              hence thesis;

            end;

            thus x in H

            proof

              per cases ;

                suppose b = ic;

                hence thesis by A3, A8, A9;

              end;

                suppose

                 A10: b <> ic;

                reconsider ic as Subset of X;

                now

                  let c be set;

                  assume that

                   A11: c in G and

                   A12: a c= c;

                  c in C by A11, A12;

                  hence ic c= c by MSSUBFAM: 2;

                end;

                then

                 A13: [a, ic] in F;

                 [a, b] <= [a, ic] by A7;

                hence thesis by A4, A5, A8, A10, A13, Th27;

              end;

            end;

          end;

          assume x in H;

          then

           A14: ex S be Subset-Family of X st ( Intersect S) = x & S c= G;

          thus x in ssF by A1, A2, A14, Th1, XBOOLE_1: 1;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    theorem :: ARMSTRNG:43

    

     Th43: for X be finite non empty set, F be Full-family of X holds ex G be Subset-Family of X st G is_generator-set_of ( saturated-subsets F) & F = (X deps_encl_by G)

    proof

      let X be finite non empty set, F be Full-family of X;

      set G = ( saturated-subsets F);

      take G;

      

       A1: G is (B1) (B2) by Th32;

      thus G is_generator-set_of G

      proof

        set H = { ( Intersect S) where S be Subset-Family of X : S c= G };

        thus G c= G;

        now

          let x be object;

          hereby

            reconsider xx = x as set by TARSKI: 1;

            set sx = {xx};

            assume

             A2: x in G;

            then

             A3: sx c= G by ZFMISC_1: 31;

            reconsider sx as Subset-Family of X by A2, ZFMISC_1: 31;

            

             A4: ( Intersect sx) = ( meet sx) by SETFAM_1:def 9;

            ( Intersect sx) in H by A3;

            hence x in H by A4, SETFAM_1: 10;

          end;

          assume x in H;

          then

           A5: ex S be Subset-Family of X st ( Intersect S) = x & S c= G;

          thus x in G by A1, A5, Th1;

        end;

        hence thesis by TARSKI: 2;

      end;

      thus thesis by A1, Th35;

    end;

    theorem :: ARMSTRNG:44

    for X be set, B be non empty finite Subset-Family of X st B is (B1) (B2) holds ( /\-IRR B) is_generator-set_of B

    proof

      let X be set, B be non empty finite Subset-Family of X;

      assume

       A1: B is (B1) (B2);

      set G = ( /\-IRR B);

      set H = { ( Intersect S) where S be Subset-Family of X : S c= G };

      thus G c= B;

      now

        let x be object;

        hereby

          assume x in B;

          then

          reconsider xx = x as Element of B;

          consider yz be non empty Subset of B such that

           A2: xx = ( meet yz) and

           A3: for s be set st s in yz holds s is_/\-irreducible_in B by Th3;

          reconsider yz as non empty Subset-Family of X by XBOOLE_1: 1;

          

           A4: yz c= G

          proof

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            assume x in yz;

            then xx is_/\-irreducible_in B by A3;

            hence thesis by Def3;

          end;

          ( Intersect yz) = ( meet yz) by SETFAM_1:def 9;

          hence x in H by A2, A4;

        end;

        assume x in H;

        then ex S be Subset-Family of X st x = ( Intersect S) & S c= G;

        hence x in B by A1, Th1, XBOOLE_1: 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ARMSTRNG:45

    for X,G be set, B be non empty finite Subset-Family of X st B is (B1) (B2) & G is_generator-set_of B holds ( /\-IRR B) c= (G \/ {X})

    proof

      let X,G be set, B be non empty finite Subset-Family of X such that

       A1: B is (B1) (B2) and

       A2: G is_generator-set_of B;

      

       A3: B = { ( Intersect S) where S be Subset-Family of X : S c= G } by A2;

      

       A4: G c= B by A2;

      let x be object;

      assume

       A5: x in ( /\-IRR B);

      then

      reconsider xx = x as Element of B;

      

       A6: xx is_/\-irreducible_in B by A5, Def3;

      assume

       A7: not x in (G \/ {X});

      then not x in {X} by XBOOLE_0:def 3;

      then

       A8: x <> X by TARSKI:def 1;

      x in B by A5;

      then

      consider S be Subset-Family of X such that

       A9: x = ( Intersect S) and

       A10: S c= G by A3;

       not x in S by A10, A7, XBOOLE_0:def 3;

      hence contradiction by A1, A4, A9, A10, A8, A6, Th4, XBOOLE_1: 1;

    end;

    begin

    definition

      let n be Element of NAT , D be non empty set;

      mode Tuple of n,D is Element of (n -tuples_on D);

    end

    theorem :: ARMSTRNG:46

    for X be non empty finite set, F be Full-family of X holds ex R be DB-Rel st the Attributes of R = X & (for a be Element of X holds (the Domains of R . a) = INT ) & F = ( Dependency-str R)

    proof

      let X be non empty finite set, F be Full-family of X;

      reconsider D = (X --> INT ) as non-empty ManySortedSet of X;

      consider G be Subset-Family of X such that G is_generator-set_of ( saturated-subsets F) and

       A1: F = (X deps_encl_by G) by Th43;

      consider H be FinSequence such that

       A2: ( rng H) = G and H is one-to-one by FINSEQ_4: 58;

       A4:

      now

        set f = (X --> 0 );

        thus ( dom f) = ( dom D);

        let x be object;

        assume

         A5: x in ( dom D);

        then (f . x) = 0 by FUNCOP_1: 7;

        then (f . x) in NAT ;

        then (f . x) in INT by NUMBERS: 17;

        hence (f . x) in (D . x) by A5, FUNCOP_1: 7;

      end;

      then

       A6: (X --> 0 ) is Element of ( product D) by CARD_3:def 5;

      reconsider H as FinSequence of G by A2, FINSEQ_1:def 4;

      per cases ;

        suppose

         A7: G is empty;

        set R = {(X --> 0 )};

        R c= ( product D)

        proof

          let x be object;

          assume x in R;

          then x = (X --> 0 ) by TARSKI:def 1;

          hence thesis by A4, CARD_3:def 5;

        end;

        then

        reconsider R as non empty Subset of ( product D);

        set BD = DB-Rel (# X, D, R #);

        take BD;

        thus the Attributes of BD = X & for a be Element of X holds (the Domains of BD . a) = INT ;

        set Ds = ( Dependency-str BD);

        now

          let x be object;

          hereby

            assume x in F;

            then

            consider A,B be Subset of X such that

             A8: x = [A, B] and for g be set st g in G & A c= g holds B c= g by A1;

            reconsider A, B as Subset of the Attributes of BD;

            A >|> (B,BD)

            proof

              let f,g be Element of the Relationship of BD;

              f = (X --> 0 ) by TARSKI:def 1;

              hence thesis by TARSKI:def 1;

            end;

            hence x in Ds by A8;

          end;

          assume x in Ds;

          then

          consider A,B be Subset of the Attributes of BD such that

           A9: x = [A, B] and A >|> (B,BD);

          for g be set st g in G & A c= g holds B c= g by A7;

          hence x in F by A1, A9;

        end;

        hence thesis by TARSKI: 2;

      end;

        suppose

         A10: G is non empty;

        then H is non empty by A2;

        then

        reconsider n = ( len H) as non zero Element of NAT ;

        defpred R[ set, Element of (n -tuples_on BOOLEAN )] means for i be Element of NAT st i in ( Seg n) holds ($1 in (H . i) implies ($2 . i) = 0 ) & ( not $1 in (H . i) implies ($2 . i) = 1);

         A11:

        now

          let x be Element of X;

          defpred P[ set, set] means (x in (H . $1) implies $2 = 0 ) & ( not x in (H . $1) implies $2 = 1);

          

           A12: for i be Nat st i in ( Seg n) holds ex x be Element of BOOLEAN st P[i, x]

          proof

            let i be Nat;

            assume i in ( Seg n);

            per cases ;

              suppose

               A13: x in (H . i);

              reconsider b = FALSE as Element of BOOLEAN ;

              take b;

              thus thesis by A13;

            end;

              suppose

               A14: not x in (H . i);

              reconsider b = TRUE as Element of BOOLEAN ;

              take b;

              thus thesis by A14;

            end;

          end;

          consider y be FinSequence of BOOLEAN such that

           A15: ( dom y) = ( Seg n) and

           A16: for i be Nat st i in ( Seg n) holds P[i, (y . i)] from FINSEQ_1:sch 5( A12);

          

           A17: y in ( BOOLEAN * ) by FINSEQ_1:def 11;

          ( len y) = n by A15, FINSEQ_1:def 3;

          then y in { s where s be Element of ( BOOLEAN * ) : ( len s) = n } by A17;

          then

          reconsider y as Element of (n -tuples_on BOOLEAN );

          take y;

          thus R[x, y] by A16;

        end;

        consider M be Function of X, (n -tuples_on BOOLEAN ) such that

         A18: for x be Element of X holds R[x, (M . x) qua Element of (n -tuples_on BOOLEAN )] from FUNCT_2:sch 3( A11);

        set R = { f where f be Element of ( product D) : ex i be Element of NAT st for x be Element of X holds (f . x) = ( Absval ((n -BinarySequence i) '&' (M . x) qua Element of (n -tuples_on BOOLEAN ))) };

        

         A19: R c= ( product D)

        proof

          let x be object;

          assume x in R;

          then ex f be Element of ( product D) st x = f & ex i be Element of NAT st for x be Element of X holds (f . x) = ( Absval ((n -BinarySequence i) '&' (M . x) qua Element of (n -tuples_on BOOLEAN )));

          hence thesis;

        end;

        now

          take i = 0 ;

          set f = (X --> 0 );

          let x be Element of X;

          

           A20: ((n -BinarySequence i) '&' (M . x) qua Element of (n -tuples_on BOOLEAN )) = (n -BinarySequence i) by Th5

          .= ( 0* n) by BINARI_3: 25;

          

          thus (f . x) = 0

          .= ( Absval ((n -BinarySequence i) '&' (M . x) qua Element of (n -tuples_on BOOLEAN ))) by A20, BINARI_3: 6;

        end;

        then (X --> 0 ) in R by A6;

        then

        reconsider R as non empty Subset of ( product D) by A19;

        set BD = DB-Rel (# X, D, R #);

        take BD;

        thus the Attributes of BD = X & for a be Element of X holds (the Domains of BD . a) = INT ;

        set Ds = ( Dependency-str BD);

        

         A21: ( dom H) = ( Seg n) by FINSEQ_1:def 3;

        now

          let x be object;

          hereby

            assume x in F;

            then

            consider A,B be Subset of X such that

             A22: x = [A, B] and

             A23: for g be set st g in G & A c= g holds B c= g by A1;

            reconsider A9 = A, B9 = B as Subset of the Attributes of BD;

            A9 >|> (B9,BD)

            proof

              let f,g be Element of the Relationship of BD;

              assume

               A24: (f | A9) = (g | A9);

              f in R;

              then

              consider Rf be Element of ( product D) such that

               A25: f = Rf and

               A26: ex i be Element of NAT st for x be Element of X holds (Rf . x) = ( Absval ((n -BinarySequence i) '&' (M . x) qua Element of (n -tuples_on BOOLEAN )));

              consider fi be Element of NAT such that

               A27: for x be Element of X holds (Rf . x) = ( Absval ((n -BinarySequence fi) '&' (M . x) qua Element of (n -tuples_on BOOLEAN ))) by A26;

              g in R;

              then

              consider Rg be Element of ( product D) such that

               A28: g = Rg and

               A29: ex i be Element of NAT st for x be Element of X holds (Rg . x) = ( Absval ((n -BinarySequence i) '&' (M . x) qua Element of (n -tuples_on BOOLEAN )));

              consider gi be Element of NAT such that

               A30: for x be Element of X holds (Rg . x) = ( Absval ((n -BinarySequence gi) '&' (M . x) qua Element of (n -tuples_on BOOLEAN ))) by A29;

              

               A31: ( dom g) = ( dom D) by A28, CARD_3: 9

              .= ( dom f) by A25, CARD_3: 9;

              now

                set nbg = (n -BinarySequence gi);

                set nbf = (n -BinarySequence fi);

                thus

                 A32: ( dom (g | B)) = (( dom f) /\ B) by A31, RELAT_1: 61;

                let a be object such that

                 A33: a in ( dom (g | B));

                reconsider x = a as Element of X by A32, A33;

                reconsider Mx = (M . x) as Tuple of n, BOOLEAN ;

                set ng = (nbg '&' (M . x) qua Element of (n -tuples_on BOOLEAN ));

                set nf = (nbf '&' (M . x) qua Element of (n -tuples_on BOOLEAN ));

                

                 A34: ( dom (M . x) qua Element of (n -tuples_on BOOLEAN )) = ( Seg n) by Lm2;

                

                 A35: ( dom nf) = ( Seg n) by Lm1;

                

                 A36: a in B by A32, A33, XBOOLE_0:def 4;

                now

                  thus ( dom nf) = ( dom ng) by A35, Lm1;

                  let i be object;

                  assume

                   A37: i in ( dom nf);

                  per cases ;

                    suppose A c= (H . i);

                    then

                     A38: B c= (H . i) by A2, A21, A23, A35, A37, FUNCT_1: 3;

                    

                     A39: (Mx /. i) = (Mx . i) by A34, A35, A37, PARTFUN1:def 6

                    .= 0 by A18, A36, A35, A37, A38;

                    

                    thus (nf . i) = ((nbf /. i) '&' (Mx /. i)) by A35, A37, Def5

                    .= ((nbg /. i) '&' (Mx /. i)) by A39

                    .= (ng . i) by A35, A37, Def5;

                  end;

                    suppose

                     A40: not A c= (H . i);

                    thus (nf . i) = (ng . i)

                    proof

                      consider xx be object such that

                       A41: xx in A and

                       A42: not xx in (H . i) by A40;

                      reconsider xx as Element of X by A41;

                      

                       A43: (f . xx) = ((g | A) . xx) by A24, A41, FUNCT_1: 49

                      .= (g . xx) by A41, FUNCT_1: 49;

                      reconsider Mxx = (M . xx) as Tuple of n, BOOLEAN ;

                      

                       A44: (f . xx) = ( Absval (nbf '&' (M . xx) qua Element of (n -tuples_on BOOLEAN ))) by A25, A27;

                      

                       A45: (g . xx) = ( Absval (nbg '&' (M . xx) qua Element of (n -tuples_on BOOLEAN ))) by A28, A30;

                      ( dom (M . xx) qua Element of (n -tuples_on BOOLEAN )) = ( Seg n) by Lm2;

                      

                      then

                       A46: (Mxx /. i) = (Mxx . i) by A35, A37, PARTFUN1:def 6

                      .= 1 by A18, A35, A37, A42;

                      

                      then

                       A47: (nbf /. i) = ((nbf /. i) '&' (Mxx /. i))

                      .= ((nbf '&' (M . xx) qua Element of (n -tuples_on BOOLEAN )) . i) by A35, A37, Def5

                      .= ((nbg '&' (M . xx) qua Element of (n -tuples_on BOOLEAN )) . i) by A43, A44, A45, BINARI_3: 2

                      .= ((nbg /. i) '&' (Mxx /. i)) by A35, A37, Def5

                      .= (nbg /. i) by A46;

                      

                      thus (nf . i) = ((nbf /. i) '&' (Mx /. i)) by A35, A37, Def5

                      .= (ng . i) by A35, A37, A47, Def5;

                    end;

                  end;

                end;

                then nf = ng by FUNCT_1: 2;

                

                then (g . a) = ( Absval ((n -BinarySequence fi) '&' (M . x) qua Element of (n -tuples_on BOOLEAN ))) by A28, A30

                .= (f . a) by A25, A27;

                hence ((g | B) . a) = (f . a) by A33, FUNCT_1: 47;

              end;

              hence thesis by FUNCT_1: 46;

            end;

            hence x in Ds by A22;

          end;

          assume x in Ds;

          then

          consider A,B be Subset of the Attributes of BD such that

           A48: x = [A, B] and

           A49: A >|> (B,BD);

          now

            deffunc F( Element of X) = ( Absval ((n -BinarySequence 0 ) '&' (M . $1) qua Element of (n -tuples_on BOOLEAN )));

            let gg be set such that

             A50: gg in G and

             A51: A c= gg and

             A52: not B c= gg;

            reconsider gg as Element of G by A50;

            consider f be Function of X, NAT such that

             A53: for x be Element of X holds (f . x) = F(x) from FUNCT_2:sch 4;

             A54:

            now

              let x be object;

              assume x in ( dom D);

              then

              reconsider x9 = x as Element of X;

              (f . x9) in INT by NUMBERS: 17;

              hence (f . x) in (D . x);

            end;

            

             A55: ( dom f) = ( dom D) by FUNCT_2:def 1;

            then

            reconsider f as Element of ( product D) by A54, CARD_3:def 5;

            consider i be Nat such that

             A56: i in ( dom H) and

             A57: (H . i) = gg by A2, A10, FINSEQ_2: 10;

            i <> 0 by A21, A56, FINSEQ_1: 1;

            then

            consider k be Nat such that

             A58: i = (k + 1) by NAT_1: 6;

            consider bx be object such that

             A59: bx in B and

             A60: not bx in gg by A52;

            reconsider bx as Element of X by A59;

            reconsider Mbx = (M . bx) as Tuple of n, BOOLEAN ;

            

             A61: f in R by A53;

            ( dom Mbx) = ( Seg n) by Lm1;

            

            then

             A62: (Mbx /. i) = (Mbx . i) by A21, A56, PARTFUN1:def 6

            .= 1 by A21, A18, A60, A56, A57;

            reconsider k as Element of NAT by ORDINAL1:def 12;

            deffunc F( Element of X) = ( Absval ((n -BinarySequence (2 to_power k)) '&' (M . $1) qua Element of (n -tuples_on BOOLEAN )));

            consider g be Function of X, NAT such that

             A63: for x be Element of X holds (g . x) = F(x) from FUNCT_2:sch 4;

             A64:

            now

              let x be object;

              assume x in ( dom D);

              then

              reconsider x9 = x as Element of X;

              (g . x9) in INT by NUMBERS: 17;

              hence (g . x) in (D . x);

            end;

            

             A65: ( dom g) = ( dom D) by FUNCT_2:def 1;

            then

            reconsider g as Element of ( product D) by A64, CARD_3:def 5;

            i <= n by A21, A56, FINSEQ_1: 1;

            then

             A66: k < n by A58, NAT_1: 13;

            now

              thus

               A67: ( dom (f | A)) = (( dom g) /\ A) by A55, A65, RELAT_1: 61;

              let x be object;

              assume

               A68: x in ( dom (f | A));

              then

              reconsider a = x as Element of X by A67;

              set bs0 = (n -BinarySequence 0 ), bsi = (n -BinarySequence (2 to_power k));

              

               A69: (g . a) = ( Absval (bsi '&' (M . a) qua Element of (n -tuples_on BOOLEAN ))) by A63;

              set L = (bs0 '&' (M . a) qua Element of (n -tuples_on BOOLEAN )), R = (bsi '&' (M . a) qua Element of (n -tuples_on BOOLEAN ));

              reconsider Ma = (M . a) as Tuple of n, BOOLEAN ;

              

               A70: x in A by A68;

               A71:

              now

                

                thus ( dom L) = ( Seg n) by Lm1

                .= ( dom R) by Lm1;

                let j be object;

                

                 A72: bs0 = ( 0* n) by BINARI_3: 25

                .= (n |-> 0 ) by EUCLID:def 4;

                assume

                 A73: j in ( dom L);

                then

                reconsider nj = j as Element of NAT ;

                

                 A74: j in ( Seg n) by A73, Lm1;

                ( dom bs0) = ( Seg n) by Lm1;

                

                then

                 A75: (bs0 /. nj) = (bs0 . nj) by A74, PARTFUN1:def 6

                .= 0 by A72;

                

                 A76: (L . j) = ((bs0 /. nj) '&' (Ma /. nj)) by A74, Def5

                .= 0 by A75;

                per cases ;

                  suppose

                   A77: i <> nj;

                  ( dom bsi) = ( Seg n) by Lm1;

                  

                  then

                   A78: (bsi /. nj) = (bsi . nj) by A74, PARTFUN1:def 6

                  .= FALSE by A58, A66, A74, A77, Th7;

                  (R . j) = ((bsi /. nj) '&' (Ma /. nj)) by A74, Def5;

                  hence (L . j) = (R . j) by A76, A78;

                end;

                  suppose

                   A79: i = nj;

                  ( dom Ma) = ( Seg n) by Lm1;

                  

                  then

                   A80: (Ma /. nj) = (Ma . i) by A74, A79, PARTFUN1:def 6

                  .= 0 by A18, A51, A57, A70, A74, A79;

                  (R . j) = ((bsi /. nj) '&' (Ma /. nj)) by A74, Def5

                  .= 0 by A80;

                  hence (L . j) = (R . j) by A76;

                end;

              end;

              ((f | A) . a) = (f . a) by A68, FUNCT_1: 49

              .= ( Absval (bs0 '&' (M . a) qua Element of (n -tuples_on BOOLEAN ))) by A53;

              hence ((f | A) . x) = (g . x) by A69, A71, FUNCT_1: 2;

            end;

            then

             A81: (f | A) = (g | A) by FUNCT_1: 46;

            set bs0 = (n -BinarySequence 0 ), bsi = (n -BinarySequence (2 to_power k));

            

             A82: bs0 = ( 0* n) by BINARI_3: 25

            .= (n |-> 0 ) by EUCLID:def 4;

            ( dom bs0) = ( Seg n) by Lm1;

            

            then

             A83: (bs0 /. i) = (bs0 . i) by A21, A56, PARTFUN1:def 6

            .= 0 by A82;

            ( dom bsi) = ( Seg n) by Lm1;

            

            then

             A84: (bsi /. i) = (bsi . i) by A21, A56, PARTFUN1:def 6

            .= 1 by A58, A66, Th7;

            

             A85: ((bsi '&' Mbx) . i) = ((bsi /. i) '&' (Mbx /. i)) by A21, A56, Def5

            .= (bsi /. i) by A62;

            

             A86: ((bs0 '&' Mbx) . i) = ((bs0 /. i) '&' (Mbx /. i)) by A21, A56, Def5

            .= (bs0 /. i) by A62;

            g in R by A63;

            then

             A87: (f | B) = (g | B) by A49, A61, A81;

            ( Absval (bs0 '&' (M . bx) qua Element of (n -tuples_on BOOLEAN ))) = (f . bx) by A53

            .= ((f | B) . bx) by A59, FUNCT_1: 49

            .= (g . bx) by A59, A87, FUNCT_1: 49

            .= ( Absval (bsi '&' (M . bx) qua Element of (n -tuples_on BOOLEAN ))) by A63;

            hence contradiction by A83, A86, A85, A84, BINARI_3: 2;

          end;

          hence x in F by A1, A48;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    begin

    

     Lm3: for X,F,BB be set st F = { [a, b] where a,b be Subset of X : for c be set st c in BB & a c= c holds b c= c } holds for x,y be Subset of X holds [x, y] in F iff for c be set st c in BB & x c= c holds y c= c

    proof

      let X,F,BB be set;

      assume

       A1: F = { [a, b] where a,b be Subset of X : for c be set st c in BB & a c= c holds b c= c };

      let x,y be Subset of X;

      hereby

        assume [x, y] in F;

        then

        consider a,b be Subset of X such that

         A2: [x, y] = [a, b] and

         A3: for c be set st c in BB & a c= c holds b c= c by A1;

        

         A4: y = b by A2, XTUPLE_0: 1;

        x = a by A2, XTUPLE_0: 1;

        hence for c be set st c in BB & x c= c holds y c= c by A3, A4;

      end;

      assume for c be set st c in BB & x c= c holds y c= c;

      hence thesis by A1;

    end;

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def26

      func candidate-keys F -> Subset-Family of X equals { A where A be Subset of X : [A, X] in ( Maximal_wrt F) };

      coherence

      proof

        set B = { A where A be Subset of X : [A, X] in ( Maximal_wrt F) };

        B c= ( bool X)

        proof

          let x be object;

          assume x in B;

          then ex A be Subset of X st x = A & [A, X] in ( Maximal_wrt F);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ARMSTRNG:47

    for X be finite set, F be Dependency-set of X, K be Subset of X st F = { [A, B] where A,B be Subset of X : K c= A or B c= A } holds ( candidate-keys F) = {K}

    proof

      let X be finite set, F be Dependency-set of X, K be Subset of X;

      assume F = { [A, B] where A,B be Subset of X : K c= A or B c= A };

      then

       A1: ( Maximal_wrt F) = ( { [K, X]} \/ { [A, A] where A be Subset of X : not K c= A }) by Th30;

      now

        let x be object;

        hereby

          assume x in ( candidate-keys F);

          then

          consider a be Subset of X such that

           A2: x = a and

           A3: [a, X] in ( Maximal_wrt F);

          per cases by A1, A3, XBOOLE_0:def 3;

            suppose [a, X] in { [K, X]};

            then [a, X] = [K, X] by TARSKI:def 1;

            then a = K by XTUPLE_0: 1;

            hence x in {K} by A2, TARSKI:def 1;

          end;

            suppose [a, X] in { [A, A] where A be Subset of X : not K c= A };

            then

            consider A be Subset of X such that

             A4: [a, X] = [A, A] and

             A5: not K c= A;

            X = A by A4, XTUPLE_0: 1;

            hence x in {K} by A5;

          end;

        end;

        assume x in {K};

        then

         A6: x = K by TARSKI:def 1;

         [K, X] in { [K, X]} by TARSKI:def 1;

        then [K, X] in ( Maximal_wrt F) by A1, XBOOLE_0:def 3;

        hence x in ( candidate-keys F) by A6;

      end;

      hence thesis by TARSKI: 2;

    end;

    notation

      let X be set;

      antonym X is (C1) for X is empty;

    end

    definition

      let X be set;

      :: ARMSTRNG:def27

      attr X is without_proper_subsets means for x,y be set st x in X & y in X & x c= y holds x = y;

    end

    notation

      let X be set;

      synonym X is (C2) for X is without_proper_subsets;

    end

    theorem :: ARMSTRNG:48

    for R be DB-Rel holds ( candidate-keys ( Dependency-str R)) is (C1) (C2)

    proof

      let D be DB-Rel;

      set F = ( Dependency-str D);

      set X = the Attributes of D;

      

       A1: F is full_family by Th23;

      then

       A2: ( Maximal_wrt F) is (M2) by Th28;

      ( saturated-subsets F) is (B1) by A1, Th32;

      then X in ( saturated-subsets F);

      then

      consider B,A be Subset of X such that

       A3: X = B and

       A4: A ^|^ (B,F) by Th31;

       [A, X] in ( Maximal_wrt F) by A3, A4;

      then A in ( candidate-keys F);

      hence ( candidate-keys F) is non empty;

      let k1,k2 be set such that

       A5: k1 in ( candidate-keys F) and

       A6: k2 in ( candidate-keys F) and

       A7: k1 c= k2;

      consider a2 be Subset of X such that

       A8: k2 = a2 and

       A9: [a2, X] in ( Maximal_wrt F) by A6;

      consider a1 be Subset of X such that

       A10: k1 = a1 and

       A11: [a1, X] in ( Maximal_wrt F) by A5;

       [a1, ( [#] X)] >= [a2, ( [#] X)] by A7, A10, A8;

      hence thesis by A10, A11, A8, A9, A2;

    end;

    theorem :: ARMSTRNG:49

    for X be finite set, C be Subset-Family of X st C is (C1) (C2) holds ex F be Full-family of X st C = ( candidate-keys F)

    proof

      let X be finite set, C be Subset-Family of X;

      set B = { b where b be Subset of X : for K be Subset of X st K in C holds not K c= b };

      

       A1: ( [#] X) = X;

      B c= ( bool X)

      proof

        let x be object;

        assume x in B;

        then ex b be Subset of X st x = b & for K be Subset of X st K in C holds not K c= b;

        hence thesis;

      end;

      then

      reconsider BB = B as Subset-Family of X;

      set F = { [a, b] where a,b be Subset of X : for c be set st c in BB & a c= c holds b c= c };

      F = (X deps_encl_by BB);

      then

      reconsider F as Full-family of X by Th33;

      assume

       A2: C is (C1);

      assume

       A3: C is (C2);

       A4:

      now

        let x be set;

        assume

         A5: x in C;

        then

        reconsider x9 = x as Subset of X;

        now

          let c be set;

          assume that

           A6: c in BB and

           A7: x9 c= c;

          ex b be Subset of X st c = b & for K be Subset of X st K in C holds not K c= b by A6;

          hence X c= c by A5, A7;

        end;

        then [x9, X] in F by A1;

        then

        consider a,b be Subset of X such that

         A8: [a, b] in ( Maximal_wrt F) and

         A9: [a, b] >= [x9, ( [#] X)] by Th26;

        

         A10: a c= x9 by A9;

        X c= b by A9;

        then

         A11: b = X by XBOOLE_0:def 10;

        assume

         A12: not [x, X] in ( Maximal_wrt F);

        now

          let K be Subset of X;

          assume

           A13: K in C;

          assume

           A14: K c= a;

          then K c= x9 by A10;

          then K = x9 by A3, A5, A13;

          hence contradiction by A8, A10, A11, A12, A14, XBOOLE_0:def 10;

        end;

        then a in BB;

        then X c= a by A8, A11, Lm3;

        then X = a by XBOOLE_0:def 10;

        hence contradiction by A8, A10, A11, A12, XBOOLE_0:def 10;

      end;

      take F;

      now

        let x be object;

        hereby

          assume

           A15: x in C;

          then [x, X] in ( Maximal_wrt F) by A4;

          hence x in ( candidate-keys F) by A15;

        end;

        assume x in ( candidate-keys F);

        then

        consider A be Subset of X such that

         A16: x = A and

         A17: [A, X] in ( Maximal_wrt F);

        assume

         A18: not x in C;

        now

          

           A19: A ^|^ (X,F) by A17;

          given K be Subset of X such that

           A20: K in C and

           A21: K c= A;

          

           A22: [K, ( [#] X)] >= [A, ( [#] X)] by A21;

           [K, X] in ( Maximal_wrt F) by A4, A20;

          hence contradiction by A16, A18, A20, A19, A22, Th27;

        end;

        then

         A23: A in BB;

        for c be set st c in BB holds c = X or not A c= c

        proof

          let c be set;

          assume that

           A24: c in BB and

           A25: not c = X;

          assume A c= c;

          then X c= c by A1, A17, A24, Lm3;

          hence contradiction by A24, A25, XBOOLE_0:def 10;

        end;

        then X in BB by A23;

        then ex b be Subset of X st b = X & for K be Subset of X st K in C holds not K c= b;

        then not ex K be object st K in C;

        hence contradiction by A2, XBOOLE_0:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ARMSTRNG:50

    for X be finite set, C be Subset-Family of X, B be set st C is (C1) (C2) & B = { b where b be Subset of X : for K be Subset of X st K in C holds not K c= b } holds C = ( candidate-keys (X deps_encl_by B))

    proof

      let X be finite set, C be Subset-Family of X, B be set such that

       A1: C is (C1) and

       A2: C is (C2) and

       A3: B = { b where b be Subset of X : for K be Subset of X st K in C holds not K c= b };

      B c= ( bool X)

      proof

        let x be object;

        assume x in B;

        then ex b be Subset of X st x = b & for K be Subset of X st K in C holds not K c= b by A3;

        hence thesis;

      end;

      then

      reconsider BB = B as Subset-Family of X;

      set F = (X deps_encl_by B);

      

       A4: ( [#] X) = X;

       A5:

      now

        let x be set;

        assume

         A6: x in C;

        then

        reconsider x9 = x as Subset of X;

        now

          let c be set;

          assume that

           A7: c in BB and

           A8: x9 c= c;

          ex b be Subset of X st c = b & for K be Subset of X st K in C holds not K c= b by A3, A7;

          hence X c= c by A6, A8;

        end;

        then [x9, X] in F by A4;

        then

        consider a,b be Subset of X such that

         A9: [a, b] in ( Maximal_wrt F) and

         A10: [a, b] >= [x9, ( [#] X)] by Th26;

        

         A11: a c= x9 by A10;

        X c= b by A10;

        then

         A12: b = X by XBOOLE_0:def 10;

        assume

         A13: not [x, X] in ( Maximal_wrt F);

        now

          let K be Subset of X;

          assume

           A14: K in C;

          assume

           A15: K c= a;

          then K c= x9 by A11;

          then K = x9 by A2, A6, A14;

          hence contradiction by A9, A11, A12, A13, A15, XBOOLE_0:def 10;

        end;

        then a in BB by A3;

        then X c= a by A9, A12, Lm3;

        then X = a by XBOOLE_0:def 10;

        hence contradiction by A9, A11, A12, A13, XBOOLE_0:def 10;

      end;

      now

        let x be object;

        hereby

          assume

           A16: x in C;

          then [x, X] in ( Maximal_wrt F) by A5;

          hence x in ( candidate-keys F) by A16;

        end;

        assume x in ( candidate-keys F);

        then

        consider A be Subset of X such that

         A17: x = A and

         A18: [A, X] in ( Maximal_wrt F);

        assume

         A19: not x in C;

        now

          

           A20: A ^|^ (X,F) by A18;

          given K be Subset of X such that

           A21: K in C and

           A22: K c= A;

          

           A23: [K, ( [#] X)] >= [A, ( [#] X)] by A22;

           [K, X] in ( Maximal_wrt F) by A5, A21;

          hence contradiction by A17, A19, A21, A20, A23, Th27;

        end;

        then

         A24: A in BB by A3;

        for c be set st c in BB holds c = X or not A c= c

        proof

          let c be set;

          assume that

           A25: c in BB and

           A26: not c = X;

          assume A c= c;

          then X c= c by A4, A18, A25, Lm3;

          hence contradiction by A25, A26, XBOOLE_0:def 10;

        end;

        then X in BB by A24;

        then ex b be Subset of X st b = X & for K be Subset of X st K in C holds not K c= b by A3;

        then not ex K be object st K in C;

        hence contradiction by A1, XBOOLE_0:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ARMSTRNG:51

    for X be non empty finite set, C be Subset-Family of X st C is (C1) (C2) holds ex R be DB-Rel st the Attributes of R = X & C = ( candidate-keys ( Dependency-str R))

    proof

      let X be non empty finite set, C be Subset-Family of X such that

       A1: C is (C1) and

       A2: C is (C2);

      reconsider D = (X --> ( bool X)) as non-empty ManySortedSet of X;

      set M = { L where L be Subset of X : for K be Subset of X st K in C holds (L /\ K) <> {} };

      reconsider M0 = (M \/ { 0 }) as non empty set;

      set R = { ((X --> 0 ) +* (L --> L)) where L be Subset of X : L in M0 };

      

       A3: R c= ( product D)

      proof

        let x be object;

        assume x in R;

        then

        consider L be Subset of X such that

         A5: x = ((X --> 0 ) +* (L --> L)) and L in M0;

        set g = ((X --> 0 ) +* (L --> L));

        

         A6: ( dom (L --> L)) = L;

         A7:

        now

          let x be object such that

           A8: x in ( dom D);

          

           A9: (D . x) = ( bool X) by A8, FUNCOP_1: 7;

          per cases ;

            suppose

             A10: x in L;

            

            then (g . x) = ((L --> L) . x) by A6, FUNCT_4: 13

            .= L by A10, FUNCOP_1: 7;

            hence (g . x) in (D . x) by A9;

          end;

            suppose not x in L;

            

            then (g . x) = ((X --> 0 ) . x) by A6, FUNCT_4: 11

            .= ( {} X);

            hence (g . x) in (D . x) by A9;

          end;

        end;

        ( dom g) = (( dom (X --> 0 )) \/ L) by A6, FUNCT_4:def 1

        .= (X \/ L)

        .= X by XBOOLE_1: 12;

        hence thesis by A5, A7, CARD_3:def 5;

      end;

       0 in { 0 } by TARSKI:def 1;

      then 0 in (M \/ { 0 }) by XBOOLE_0:def 3;

      then ((X --> 0 ) +* (( {} X) --> ( {} X))) in R;

      then

      reconsider R as non empty Subset of ( product D) by A3;

      take DB = DB-Rel (# X, D, R #);

      thus the Attributes of DB = X;

      set ds = ( Dependency-str DB);

      set ck = { A where A be Subset of X : [A, X] in ( Maximal_wrt ds) };

      

       A11: ( [#] X) = X;

       A12:

      now

        let x be set;

        assume

         A13: x in C;

        then

        reconsider A = x as Subset of X;

        reconsider AA = A, XA = X as Subset of the Attributes of DB by A11;

        now

          let f,g be Element of the Relationship of DB such that

           A14: (f | A) = (g | A);

          f in R;

          then

          consider Lf be Subset of X such that

           A15: f = ((X --> 0 ) +* (Lf --> Lf)) and

           A16: Lf in M0;

          

           A17: Lf in M or Lf in { 0 } by A16, XBOOLE_0:def 3;

          

           A18: ( dom (Lf --> Lf)) = Lf;

          g in R;

          then

          consider Lg be Subset of X such that

           A19: g = ((X --> 0 ) +* (Lg --> Lg)) and

           A20: Lg in M0;

          

           A21: Lg in M or Lg in { 0 } by A20, XBOOLE_0:def 3;

          

           A22: ( dom (Lg --> Lg)) = Lg;

          per cases by A17, A21, TARSKI:def 1;

            suppose Lf in M & Lg in M;

            then ex Lff be Subset of X st Lf = Lff & for K be Subset of X st K in C holds (Lff /\ K) <> {} ;

            then

             A23: (Lf /\ A) <> {} by A13;

            then

            consider a be object such that

             A24: a in (Lf /\ A) by XBOOLE_0:def 1;

            

             A25: (g . a) = 0 or (g . a) = Lg

            proof

              per cases ;

                suppose

                 A26: a in Lg;

                then (g . a) = ((Lg --> Lg) . a) by A19, A22, FUNCT_4: 13;

                hence thesis by A26, FUNCOP_1: 7;

              end;

                suppose not a in Lg;

                then (g . a) = ((X --> 0 ) . a) by A19, A22, FUNCT_4: 11;

                hence thesis;

              end;

            end;

            

             A27: a in Lf by A24, XBOOLE_0:def 4;

            

             A28: a in A by A24, XBOOLE_0:def 4;

            then

             A29: ((g | A) . a) = (g . a) by FUNCT_1: 49;

            ((f | A) . a) = (f . a) by A28, FUNCT_1: 49

            .= ((Lf --> Lf) . a) by A15, A18, A27, FUNCT_4: 13

            .= Lf by A27, FUNCOP_1: 7;

            hence (f | X) = (g | X) by A14, A15, A19, A23, A29, A25;

          end;

            suppose

             A30: Lf in M & Lg = 0 ;

            then ex L be Subset of X st Lf = L & for K be Subset of X st K in C holds (L /\ K) <> {} ;

            then

             A31: (Lf /\ A) <> {} by A13;

            then

            consider a be object such that

             A32: a in (Lf /\ A) by XBOOLE_0:def 1;

            

             A33: a in A by A32, XBOOLE_0:def 4;

            

            then

             A34: ((g | A) . a) = (g . a) by FUNCT_1: 49

            .= (((X --> 0 ) +* {} ) . a) by A19, A30

            .= ((X --> 0 ) . a)

            .= {} ;

            

             A35: a in Lf by A32, XBOOLE_0:def 4;

            ((f | A) . a) = (f . a) by A33, FUNCT_1: 49

            .= ((Lf --> Lf) . a) by A15, A18, A35, FUNCT_4: 13

            .= Lf by A35, FUNCOP_1: 7;

            hence (f | X) = (g | X) by A14, A31, A34;

          end;

            suppose

             A36: Lf = 0 & Lg in M;

            then ex L be Subset of X st Lg = L & for K be Subset of X st K in C holds (L /\ K) <> {} ;

            then

             A37: (Lg /\ A) <> {} by A13;

            then

            consider a be object such that

             A38: a in (Lg /\ A) by XBOOLE_0:def 1;

            

             A39: a in A by A38, XBOOLE_0:def 4;

            

            then

             A40: ((f | A) . a) = (f . a) by FUNCT_1: 49

            .= (((X --> 0 ) +* {} ) . a) by A15, A36

            .= ((X --> 0 ) . a)

            .= {} ;

            

             A41: a in Lg by A38, XBOOLE_0:def 4;

            ((g | A) . a) = (g . a) by A39, FUNCT_1: 49

            .= ((Lg --> Lg) . a) by A19, A22, A41, FUNCT_4: 13

            .= Lg by A41, FUNCOP_1: 7;

            hence (f | X) = (g | X) by A14, A37, A40;

          end;

            suppose Lf = 0 & Lg = 0 ;

            hence (f | X) = (g | X) by A15, A19;

          end;

        end;

        then AA >|> (XA,DB);

        then [A, X] in ds;

        then

        consider a,b be Subset of X such that

         A42: [a, b] in ( Maximal_wrt ds) and

         A43: [a, b] >= [A, ( [#] X)] by Th26;

        

         A44: a c= A by A43;

         [a, b] in ds by A42;

        then

        consider aa,XX be Subset of the Attributes of DB such that

         A45: [a, b] = [aa, XX] and

         A46: aa >|> (XX,DB);

        

         A47: a = aa by A45, XTUPLE_0: 1;

        

         A48: b = XX by A45, XTUPLE_0: 1;

        

         A49: X c= b by A43;

        then

         A50: b = X by XBOOLE_0:def 10;

        now

          set r1 = ((X --> 0 ) +* ((a ` ) --> (a ` )));

          set r0 = (X --> 0 );

          assume

           A51: a <> A;

           A52:

          now

            assume (a ` ) = {} ;

            then (a ` ) c= a;

            then a = X by A11, SUBSET_1: 19;

            hence contradiction by A44, A51, XBOOLE_0:def 10;

          end;

          then

          consider y be object such that

           A53: y in (a ` ) by XBOOLE_0:def 1;

          now

            let K be Subset of X;

            assume

             A54: K in C;

            assume ((a ` ) /\ K) = {} ;

            then K misses (a ` ) by XBOOLE_0:def 7;

            then

             A55: K c= a by SUBSET_1: 24;

            then K c= A by A44;

            then K = A by A2, A13, A54;

            hence contradiction by A44, A51, A55, XBOOLE_0:def 10;

          end;

          then (a ` ) in M;

          then (a ` ) in M0 by XBOOLE_0:def 3;

          then

           A56: r1 in R;

           0 in { 0 } by TARSKI:def 1;

          then 0 in M0 by XBOOLE_0:def 3;

          then ((X --> 0 ) +* (( {} X) --> ( {} X))) in R;

          then ((X --> 0 ) +* {} ) in R;

          then

          reconsider r0, r1 as Element of the Relationship of DB by A56;

          

           A57: ((r0 | X) . y) = (r0 . y)

          .= 0 ;

          

           A58: ( dom ((a ` ) --> (a ` ))) = (a ` );

          now

            

             A59: ( dom r1) = (( dom (X --> 0 )) \/ ( dom ((a ` ) --> (a ` )))) by FUNCT_4:def 1

            .= (X \/ ( dom ((a ` ) --> (a ` ))))

            .= (X \/ (a ` ))

            .= X by XBOOLE_1: 12;

            ( dom r0) = X;

            hence ( dom (r0 | a)) = (( dom r1) /\ a) by A59, RELAT_1: 61;

            let x be object;

            assume

             A60: x in ( dom (r0 | a));

            ( dom (r0 | a)) = (( dom r0) /\ a) by RELAT_1: 61;

            then

             A61: x in a by A60, XBOOLE_0:def 4;

            a misses (a ` ) by XBOOLE_1: 79;

            then (a /\ (a ` )) = {} by XBOOLE_0:def 7;

            then

             A62: not x in (a ` ) by A61, XBOOLE_0:def 4;

            

            thus ((r0 | a) . x) = ((X --> 0 ) . x) by A61, FUNCT_1: 49

            .= (r1 . x) by A58, A62, FUNCT_4: 11;

          end;

          then

           A63: (r0 | a) = (r1 | a) by FUNCT_1: 46;

          ((r1 | X) . y) = (r1 . y) by A53, FUNCT_1: 49

          .= (((a ` ) --> (a ` )) . y) by A58, A53, FUNCT_4: 13

          .= (a ` ) by A53, FUNCOP_1: 7;

          hence contradiction by A50, A46, A47, A48, A63, A52, A57;

        end;

        then [A, X] in ( Maximal_wrt ds) by A42, A49, XBOOLE_0:def 10;

        hence x in ck;

      end;

      now

        let x be object;

        thus x in C implies x in ck by A12;

        assume x in ck;

        then

        consider A be Subset of X such that

         A64: x = A and

         A65: [A, X] in ( Maximal_wrt ds);

         [A, X] in ds by A65;

        then

        consider aa,XX be Subset of the Attributes of DB such that

         A66: [A, X] = [aa, XX] and

         A67: aa >|> (XX,DB);

        

         A68: X = XX by A66, XTUPLE_0: 1;

         A69:

        now

          

           A70: A ^|^ (( [#] X),ds) by A65;

          let K be set such that

           A71: K in C and

           A72: K c= A;

          K in ck by A12, A71;

          then

          consider B be Subset of X such that

           A73: K = B and

           A74: [B, X] in ( Maximal_wrt ds);

          assume

           A75: K <> A;

          reconsider AA = A, B, XA = X as Subset of the Attributes of DB by A11;

           [AA, XA] <= [B, XA] by A72, A73;

          hence contradiction by A73, A74, A75, A70, Th27;

        end;

        set m = { a where a be Element of X : not a in A & ex K be set st K in C & a in K };

         A76:

        now

          let x be object;

          assume x in m;

          then ex a be Element of X st x = a & not a in A & ex K be set st K in C & a in K;

          hence x in X;

        end;

        consider K be object such that

         A77: K in C by A1, XBOOLE_0:def 1;

        reconsider K as Subset of X by A77;

        

         A78: A = aa by A66, XTUPLE_0: 1;

        assume

         A79: not x in C;

        then not K c= A by A64, A69, A77;

        then

        consider k be object such that

         A80: k in K and

         A81: not k in A;

        reconsider k as Element of X by A80;

        

         A82: k in m by A77, A80, A81;

        then

        consider n be object such that

         A83: n in m;

        reconsider m as Subset of X by A76, TARSKI:def 3;

        set r0 = (X --> 0 ), r1 = ((X --> 0 ) +* (m --> m));

        now

          let K be Subset of X such that

           A84: K in C;

           not K c= A by A64, A69, A79, A84;

          then

          consider k be object such that

           A85: k in K and

           A86: not k in A;

          k in m by A84, A85, A86;

          hence (m /\ K) <> {} by A85, XBOOLE_0:def 4;

        end;

        then m in M;

        then m in M0 by XBOOLE_0:def 3;

        then

         A87: r1 in R;

         0 in { 0 } by TARSKI:def 1;

        then 0 in M0 by XBOOLE_0:def 3;

        then ((X --> 0 ) +* (( {} X) --> ( {} X))) in R;

        then ((X --> 0 ) +* {} ) in R;

        then

        reconsider r0, r1 as Element of the Relationship of DB by A87;

        

         A88: ( dom (m --> m)) = m;

        now

          

           A89: ( dom r1) = (( dom (X --> 0 )) \/ ( dom (m --> m))) by FUNCT_4:def 1

          .= (X \/ ( dom (m --> m)))

          .= (X \/ m)

          .= X by XBOOLE_1: 12;

          ( dom r0) = X;

          hence ( dom (r0 | A)) = (( dom r1) /\ A) by A89, RELAT_1: 61;

          

           A90: ( dom (r0 | A)) = (( dom r0) /\ A) by RELAT_1: 61;

          let x be object such that

           A91: x in ( dom (r0 | A));

           A92:

          now

            assume x in m;

            then ex a be Element of X st x = a & not a in A & ex K be set st K in C & a in K;

            hence contradiction by A90, A91, XBOOLE_0:def 4;

          end;

          x in A by A90, A91, XBOOLE_0:def 4;

          

          hence ((r0 | A) . x) = ((X --> 0 ) . x) by FUNCT_1: 49

          .= (r1 . x) by A88, A92, FUNCT_4: 11;

        end;

        then

         A93: (r0 | A) = (r1 | A) by FUNCT_1: 46;

        

         A94: ((r1 | X) . n) = (r1 . n) by A83, FUNCT_1: 49

        .= ((m --> m) . n) by A83, A88, FUNCT_4: 13

        .= m by A83, FUNCOP_1: 7;

        ((r0 | X) . n) = (r0 . n)

        .= 0 ;

        hence contradiction by A82, A93, A67, A78, A68, A94;

      end;

      hence thesis by TARSKI: 2;

    end;

    begin

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def28

      attr F is (DC4) means for A,B,C be Subset of X st [A, B] in F & [A, C] in F holds [A, (B \/ C)] in F;

      :: ARMSTRNG:def29

      attr F is (DC5) means for A,B,C,D be Subset of X st [A, B] in F & [(B \/ C), D] in F holds [(A \/ C), D] in F;

      :: ARMSTRNG:def30

      attr F is (DC6) means for A,B,C be Subset of X st [A, B] in F holds [(A \/ C), B] in F;

    end

    theorem :: ARMSTRNG:52

    for X be set, F be Dependency-set of X holds F is (F1) (F2) (F3) (F4) iff F is (F2) (DC3) (F4);

    theorem :: ARMSTRNG:53

    for X be set, F be Dependency-set of X holds F is (F1) (F2) (F3) (F4) iff F is (DC1) (DC3) (DC4)

    proof

      let X be set, F be Dependency-set of X;

      hereby

        assume that

         A1: F is (F1) and

         A2: F is (F2) and

         A3: F is (F3) and

         A4: F is (F4);

        thus F is (DC1) by A2;

        thus F is (DC3) by A1, A3;

        thus F is (DC4)

        proof

          let A,B,C be Subset of X;

          assume that

           A5: [A, B] in F and

           A6: [A, C] in F;

           [(A \/ A), (B \/ C)] in F by A4, A5, A6;

          hence thesis;

        end;

      end;

      assume that

       A7: F is (DC1) and

       A8: F is (DC3) and

       A9: F is (DC4);

      thus F is (F1) by A8;

      thus F is (F2) by A7;

      thus F is (F3) by A7, A8;

      let A,B,A9,B9 be Subset of X such that

       A10: [A, B] in F and

       A11: [A9, B9] in F;

      A9 c= (A \/ A9) by XBOOLE_1: 7;

      then [(A \/ A9), A9] in F by A8;

      then

       A12: [(A \/ A9), B9] in F by A7, A11, Th18;

      A c= (A \/ A9) by XBOOLE_1: 7;

      then [(A \/ A9), A] in F by A8;

      then [(A \/ A9), B] in F by A7, A10, Th18;

      hence thesis by A9, A12;

    end;

    theorem :: ARMSTRNG:54

    for X be set, F be Dependency-set of X holds F is (F1) (F2) (F3) (F4) iff F is (DC2) (DC5) (DC6)

    proof

      let X be set, F be Dependency-set of X;

      hereby

        assume that

         A1: F is (F1) and

         A2: F is (F2) and

         A3: F is (F3) and

         A4: F is (F4);

        thus F is (DC2) by A1;

        thus F is (DC5)

        proof

          let A,B,C,D be Subset of X such that

           A5: [A, B] in F and

           A6: [(B \/ C), D] in F;

           [C, C] in F by A1;

          then [(A \/ C), (B \/ C)] in F by A4, A5;

          hence thesis by A2, A6, Th18;

        end;

        thus F is (DC6)

        proof

          let A,B,C be Subset of X such that

           A7: [A, B] in F;

          A c= (A \/ C) by XBOOLE_1: 7;

          then [(A \/ C), A] in F by A1, A3, Def15;

          hence thesis by A2, A7, Th18;

        end;

      end;

      assume that

       A8: F is (DC2) and

       A9: F is (DC5) and

       A10: F is (DC6);

      thus F is (F1) by A8;

       A11:

      now

        let A,B,C be Subset of X such that

         A12: [A, B] in F and

         A13: [B, C] in F;

         [(B \/ A), C] in F by A10, A13;

        then [(A \/ A), C] in F by A9, A12;

        hence [A, C] in F;

      end;

      hence F is (F2) by Th18;

      thus F is (F3)

      proof

        let A,B,A9,B9 be Subset of X such that

         A14: [A, B] in F and

         A15: [A, B] >= [A9, B9];

        A c= A9 by A15;

        then A9 = (A \/ (A9 \ A)) by XBOOLE_1: 45;

        then

         A16: [A9, B] in F by A10, A14;

        B9 c= B by A15;

        then

         A17: B = (B9 \/ (B \ B9)) by XBOOLE_1: 45;

         [B9, B9] in F by A8;

        then [B, B9] in F by A10, A17;

        hence thesis by A11, A16;

      end;

      let A,B,A9,B9 be Subset of X such that

       A18: [A, B] in F and

       A19: [A9, B9] in F;

       [(B \/ B9), (B \/ B9)] in F by A8;

      then [(A \/ B9), (B \/ B9)] in F by A9, A18;

      hence thesis by A9, A19;

    end;

    definition

      let X be set, F be Dependency-set of X;

      :: ARMSTRNG:def31

      func charact_set F -> set equals { A where A be Subset of X : ex a,b be Subset of X st [a, b] in F & a c= A & not b c= A };

      correctness ;

    end

    theorem :: ARMSTRNG:55

    

     Th55: for X,A be set, F be Dependency-set of X st A in ( charact_set F) holds A is Subset of X & ex a,b be Subset of X st [a, b] in F & a c= A & not b c= A

    proof

      let X,A be set, F be Dependency-set of X;

      assume A in ( charact_set F);

      then ex Y be Subset of X st A = Y & ex a,b be Subset of X st [a, b] in F & a c= Y & not b c= Y;

      hence thesis;

    end;

    theorem :: ARMSTRNG:56

    for X be set, A be Subset of X, F be Dependency-set of X st ex a,b be Subset of X st [a, b] in F & a c= A & not b c= A holds A in ( charact_set F);

    theorem :: ARMSTRNG:57

    

     Th57: for X be finite non empty set, F be Dependency-set of X holds (for A,B be Subset of X holds [A, B] in ( Dependency-closure F) iff for a be Subset of X st A c= a & not B c= a holds a in ( charact_set F)) & ( saturated-subsets ( Dependency-closure F)) = (( bool X) \ ( charact_set F))

    proof

      let A be finite non empty set, F be Dependency-set of A;

      set G = ( Dependency-closure F);

      set B = (( bool A) \ ( charact_set F));

      set BB = { b where b be Subset of A : for x,y be Subset of A st [x, y] in F & x c= b holds y c= b };

      now

        let c be object;

        reconsider cc = c as set by TARSKI: 1;

        hereby

          assume

           A1: c in B;

          then not c in ( charact_set F) by XBOOLE_0:def 5;

          then for x,y be Subset of A st [x, y] in F & x c= cc holds y c= cc by A1;

          hence c in BB by A1;

        end;

        assume c in BB;

        then

        consider b be Subset of A such that

         A2: c = b and

         A3: for x,y be Subset of A st [x, y] in F & x c= b holds y c= b;

         not b in ( charact_set F) by A3, Th55;

        hence c in B by A2, XBOOLE_0:def 5;

      end;

      then

       A4: B = BB by TARSKI: 2;

      reconsider B as Subset-Family of A;

      

       A5: BB = ( enclosure_of F);

      then

       A6: B is (B2) by A4, Th36;

      set FF = { [a, b] where a,b be Subset of A : for c be set st c in B & a c= c holds b c= c };

      

       A7: FF = (A deps_encl_by B);

      then

      reconsider FF as Dependency-set of A;

      F c= G by Def24;

      then

       A8: FF c= G by A4, A5, A7, Th37;

      

       A9: FF is full_family by A7, Th33;

      F c= FF by A4, A5, A7, Th37;

      then

       A10: G c= FF by A9, Def24;

      hereby

        let X,Y be Subset of A;

        hereby

          assume [X, Y] in G;

          then [X, Y] in FF by A10;

          then

          consider a9,b9 be Subset of A such that

           A11: [a9, b9] = [X, Y] and

           A12: for c be set st c in B & a9 c= c holds b9 c= c;

          

           A13: b9 = Y by A11, XTUPLE_0: 1;

          let a be Subset of A such that

           A14: X c= a and

           A15: not Y c= a;

          assume not a in ( charact_set F);

          then

           A16: a in B by XBOOLE_0:def 5;

          a9 = X by A11, XTUPLE_0: 1;

          hence contradiction by A14, A15, A12, A13, A16;

        end;

        assume

         A17: for a be Subset of A st X c= a & not Y c= a holds a in ( charact_set F);

        now

          let c be set such that

           A18: c in B and

           A19: X c= c and

           A20: not Y c= c;

          reconsider c as Subset of A by A18;

           not c in ( charact_set F) by A18, XBOOLE_0:def 5;

          hence contradiction by A17, A19, A20;

        end;

        then [X, Y] in FF;

        hence [X, Y] in G by A8;

      end;

      for x,y be Subset of A st [x, y] in F & x c= A holds y c= A;

      then not ( [#] A) in ( charact_set F) by Th55;

      then A in B by XBOOLE_0:def 5;

      then

       A21: B is (B1);

      G = FF by A10, A8, XBOOLE_0:def 10;

      hence thesis by A21, A6, A7, Th35;

    end;

    theorem :: ARMSTRNG:58

    for X be finite non empty set, F,G be Dependency-set of X st ( charact_set F) = ( charact_set G) holds ( Dependency-closure F) = ( Dependency-closure G)

    proof

      let A be finite non empty set, F,G be Dependency-set of A such that

       A1: ( charact_set F) = ( charact_set G);

      set DCF = ( Dependency-closure F), DCG = ( Dependency-closure G);

      now

        let x be object;

        hereby

          assume

           A2: x in DCF;

          then

          consider a,b be Subset of A such that

           A3: x = [a, b] by Th9;

          for c be Subset of A st a c= c & not b c= c holds c in ( charact_set G) by A1, A2, A3, Th57;

          hence x in DCG by A3, Th57;

        end;

        assume

         A4: x in DCG;

        then

        consider a,b be Subset of A such that

         A5: x = [a, b] by Th9;

        for c be Subset of A st a c= c & not b c= c holds c in ( charact_set F) by A1, A4, A5, Th57;

        hence x in DCF by A5, Th57;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ARMSTRNG:59

    

     Th59: for X be non empty finite set, F be Dependency-set of X holds ( charact_set F) = ( charact_set ( Dependency-closure F))

    proof

      let X be non empty finite set, F be Dependency-set of X;

      set dcF = ( Dependency-closure F);

      now

        set B = { c where c be Subset of X : for x,y be Subset of X st [x, y] in F & x c= c holds y c= c };

        let A be object;

        reconsider AA = A as set by TARSKI: 1;

        hereby

          

           A1: F c= dcF by Def24;

          assume

           A2: A in ( charact_set F);

          then

           A3: A is Subset of X by Th55;

          ex x,y be Subset of X st [x, y] in F & x c= AA & not y c= AA by A2, Th55;

          hence A in ( charact_set dcF) by A1, A3;

        end;

        assume

         A4: A in ( charact_set dcF);

        then

        consider x,y be Subset of X such that

         A5: [x, y] in dcF and

         A6: x c= AA and

         A7: not y c= AA by Th55;

        

         A8: A is Subset of X by A4, Th55;

        assume not A in ( charact_set F);

        then for x,y be Subset of X st [x, y] in F & x c= AA holds y c= AA by A8;

        then

         A9: A in B by A8;

        B = ( enclosure_of F);

        then ( Dependency-closure F) = (X deps_encl_by B) by Th38;

        then

        consider a,b be Subset of X such that

         A10: [x, y] = [a, b] and

         A11: for c be set st c in B & a c= c holds b c= c by A5;

        

         A12: y = b by A10, XTUPLE_0: 1;

        x = a by A10, XTUPLE_0: 1;

        hence contradiction by A6, A7, A11, A12, A9;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let A be set, K be set, F be Dependency-set of A;

      :: ARMSTRNG:def32

      pred K is_p_i_w_ncv_of F means (for a be Subset of A st K c= a & a <> A holds a in ( charact_set F)) & for k be set st k c< K holds ex a be Subset of A st k c= a & a <> A & not a in ( charact_set F);

    end

    theorem :: ARMSTRNG:60

    for X be finite non empty set, F be Dependency-set of X, K be Subset of X holds K in ( candidate-keys ( Dependency-closure F)) iff K is_p_i_w_ncv_of F

    proof

      let X be finite non empty set, F be Dependency-set of X, K be Subset of X;

      set dcF = ( Dependency-closure F);

      set S = { P where P be Subset of X : [K, P] in dcF };

      S c= ( bool X)

      proof

        let x be object;

        assume x in S;

        then ex P be Subset of X st x = P & [K, P] in dcF;

        hence thesis;

      end;

      then

      reconsider S as Subset-Family of X;

      set ck = ( candidate-keys dcF);

      set B = { c where c be Subset of X : for x,y be Subset of X st [x, y] in F & x c= c holds y c= c };

       [K, K] in dcF by Def11;

      then K in S;

      then

      consider m be set such that

       A1: m in S and

       A2: for B be set st B in S holds m c= B implies B = m by FINSET_1: 6;

      B = ( enclosure_of F);

      then

       A3: dcF = (X deps_encl_by B) by Th38;

      hereby

        assume K in ck;

        then

        consider A be Subset of X such that

         A4: K = A and

         A5: [A, X] in ( Maximal_wrt dcF);

        

         A6: A ^|^ (X,dcF) by A5;

         [A, ( [#] X)] in dcF by A5;

        then

        consider a,b be Subset of X such that

         A7: [A, X] = [a, b] and

         A8: for c be set st c in B & a c= c holds b c= c by A3;

        

         A9: X = b by A7, XTUPLE_0: 1;

        

         A10: A = a by A7, XTUPLE_0: 1;

        thus K is_p_i_w_ncv_of F

        proof

          hereby

            let z be Subset of X such that

             A11: K c= z and

             A12: z <> X and

             A13: not z in ( charact_set F);

            for x,y be Subset of X st [x, y] in F & x c= z holds y c= z by A13;

            then z in B;

            then X c= z by A4, A8, A10, A9, A11;

            hence contradiction by A12, XBOOLE_0:def 10;

          end;

          let k be set;

          assume

           A14: k c< K;

          then k c= A by A4, XBOOLE_0:def 8;

          then

          reconsider k as Subset of X by XBOOLE_1: 1;

          set S = { P where P be Subset of X : [k, P] in dcF };

          S c= ( bool X)

          proof

            let x be object;

            assume x in S;

            then ex P be Subset of X st x = P & [k, P] in dcF;

            hence thesis;

          end;

          then

          reconsider S as Subset-Family of X;

           [k, k] in dcF by Def11;

          then k in S;

          then

          consider m be set such that

           A15: m in S and

           A16: for B be set st B in S holds m c= B implies B = m by FINSET_1: 6;

          consider P be Subset of X such that

           A17: m = P and

           A18: [k, P] in dcF by A15;

           [k, k] in dcF by Def11;

          then

           A19: [(k \/ k), (k \/ P)] in dcF by A18, Def13;

          assume

           A20: not thesis;

          

           A21: [k, ( [#] X)] in dcF

          proof

            per cases ;

              suppose (k \/ P) = X;

              hence thesis by A19;

            end;

              suppose (k \/ P) <> X;

              then (k \/ P) in ( charact_set F) by A20, XBOOLE_1: 7;

              then (k \/ P) in ( charact_set dcF) by Th59;

              then

              consider x,y be Subset of X such that

               A22: [x, y] in dcF and

               A23: x c= (k \/ P) and

               A24: not y c= (k \/ P) by Th55;

               [(k \/ P), (k \/ P)] in dcF by Def11;

              then [(x \/ (k \/ P)), (y \/ (k \/ P))] in dcF by A22, Def13;

              then [(k \/ P), (y \/ (k \/ P))] in dcF by A23, XBOOLE_1: 12;

              then [k, (y \/ (k \/ P))] in dcF by A19, Th18;

              then

               A25: (y \/ (k \/ P)) in S;

              P c= (k \/ P) by XBOOLE_1: 7;

              then P = (y \/ (k \/ P)) by A16, A17, A25, XBOOLE_1: 10;

              hence thesis by A24, XBOOLE_1: 7, XBOOLE_1: 10;

            end;

          end;

          k c= K by A14, XBOOLE_0:def 8;

          then [K, ( [#] X)] <= [k, ( [#] X)];

          hence contradiction by A4, A6, A14, A21, Th27;

        end;

      end;

      consider P be Subset of X such that

       A26: m = P and

       A27: [K, P] in dcF by A1;

       [K, K] in dcF by Def11;

      then

       A28: [(K \/ K), (K \/ P)] in dcF by A27, Def13;

      assume

       A29: K is_p_i_w_ncv_of F;

      

       A30: K c= (K \/ P) by XBOOLE_1: 7;

      

       A31: [K, ( [#] X)] in dcF

      proof

        per cases ;

          suppose (K \/ P) = X;

          hence thesis by A28;

        end;

          suppose (K \/ P) <> X;

          then (K \/ P) in ( charact_set F) by A29, A30;

          then (K \/ P) in ( charact_set dcF) by Th59;

          then

          consider x,y be Subset of X such that

           A32: [x, y] in dcF and

           A33: x c= (K \/ P) and

           A34: not y c= (K \/ P) by Th55;

           [(K \/ P), (K \/ P)] in dcF by Def11;

          then [(x \/ (K \/ P)), (y \/ (K \/ P))] in dcF by A32, Def13;

          then [(K \/ P), (y \/ (K \/ P))] in dcF by A33, XBOOLE_1: 12;

          then [K, (y \/ (K \/ P))] in dcF by A28, Th18;

          then

           A35: (y \/ (K \/ P)) in S;

          P c= (K \/ P) by XBOOLE_1: 7;

          then P = (y \/ (K \/ P)) by A2, A26, A35, XBOOLE_1: 10;

          hence thesis by A34, XBOOLE_1: 7, XBOOLE_1: 10;

        end;

      end;

      now

        let x9,y9 be Subset of X such that

         A36: [x9, y9] in dcF and

         A37: K <> x9 or X <> y9 and

         A38: [K, ( [#] X)] <= [x9, y9];

        

         A39: X c= y9 by A38;

        x9 c= K by A38;

        then x9 c< K by A37, A39, XBOOLE_0:def 8, XBOOLE_0:def 10;

        then

        consider a be Subset of X such that

         A40: x9 c= a and

         A41: a <> X and

         A42: not a in ( charact_set F) by A29;

        X = y9 by A39, XBOOLE_0:def 10;

        then

         A43: not y9 c= a by A41, XBOOLE_0:def 10;

         not a in ( charact_set dcF) by A42, Th59;

        hence contradiction by A36, A40, A43;

      end;

      then K ^|^ (X,dcF) by A31, Th27;

      then [K, X] in ( Maximal_wrt dcF);

      hence thesis;

    end;