:: Armstrong's Axioms
::  by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_2, FINSEQ_1, RELAT_1,
      FINSUB_1, FINSET_1, SETFAM_1, TARSKI, RELAT_2, WAYBEL_4, ORDERS_2,
      STRUCT_0, XXREAL_0, NAT_1, CARD_1, PRE_POLY, FUNCT_1, MARGREL1, XBOOLEAN,
      PARTFUN1, BINARI_3, EUCLID, ARYTM_3, POWER, ORDINAL4, PBOOLE, CARD_3,
      ZFMISC_1, MCART_1, EQREL_1, FUNCOP_1, BINARITH, FUNCT_4, ARMSTRNG;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, FINSET_1, FINSUB_1, RELAT_1,
      RELAT_2, RELSET_1, SETFAM_1, PARTFUN1, CARD_1, NUMBERS, FUNCT_4, FUNCT_1,
      ORDERS_2, MCART_1, EQREL_1, CARD_3, PBOOLE, STRUCT_0, WAYBEL_4, FINSEQ_1,
      FUNCOP_1, MARGREL1, FINSEQ_2, BINARITH, BINARI_3, SERIES_1, EUCLID,
      XXREAL_0, ORDINAL1, NAT_1, PRE_POLY, FUNCT_2;
 constructors SETFAM_1, XXREAL_0, FINSEQOP, SERIES_1, BINARITH, EUCLID,
      MATRLIN, WAYBEL_4, BINARI_3, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, EQREL_1, MARGREL1,
      FINSEQ_2, CARD_3, ORDERS_2, PRE_POLY, CARD_1, RELSET_1, STRUCT_0,
      FUNCT_4, XTUPLE_0;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
 definitions TARSKI, RELAT_2, YELLOW_0, WAYBEL_4, FINSUB_1, FINSEQ_2, SUBSET_1,
      XBOOLEAN, PRE_POLY, XTUPLE_0;
 theorems TARSKI, RELSET_1, ZFMISC_1, EQREL_1, MCART_1, RELAT_1, RELAT_2,
      XBOOLE_0, XBOOLE_1, ORDERS_2, ENUMSET1, BAGORDER, WAYBEL_4, FINSET_1,
      SUBSET_1, SETFAM_1, MSSUBFAM, TREES_1, FUNCT_1, FINSEQ_4, FINSEQ_1,
      FINSEQ_2, FUNCOP_1, CARD_3, BINARI_3, NAT_1, EUCLID, FUNCT_2, BINARITH,
      POWER, FUNCT_4, FINSUB_1, PARTFUN1, NUMBERS, XREAL_1, ORDERS_1, XXREAL_0,
      ORDINAL1, PRE_POLY, CARD_1, XTUPLE_0;
 schemes FINSET_1, NAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, XBOOLE_0, CLASSES1;

begin

Lm1: now
  let n be Element of 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 Th1:
  for B being set st B is cap-closed for X being set, S being
  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 being 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,FINSUB_1:def 2;
    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 set;
      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 set;
      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 set;
      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 Th2:
  for R being antisymmetric transitive non empty Relation, X being
finite Subset of field R st X <> {} ex x being Element of X st x is_maximal_wrt
  X, R
proof
  let R be antisymmetric transitive non empty Relation, X being 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,RELAT_2:def 8;
    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,RELAT_2:def 4;
  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 being 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 being set such that
A13: y in X and
A14: y <> x and
A15: [x, y] in R;
  thus thesis by A12,A13,A14,A15,WAYBEL_4:def 23;
end;

scheme
  SubsetSEq { X() -> set, P[set] }: for X1,X2 being Subset of X() st (for y
  being set holds y in X1 iff P[y]) & (for y being set holds y in X2 iff P[y])
  holds X1 = X2 proof
  let X1,X2 being Subset of X() such that
A1: for y being set holds y in X1 iff P[y] and
A2: for y being set holds y in X2 iff P[y];
  for x being set holds x in X1 iff x in X2
  proof
    let x be set;
    hereby
      assume x in X1;
      then P[x] by A1;
      hence x in X2 by A2;
    end;
    assume x in X2;
    then P[x] by A2;
    hence thesis by A1;
  end;
  hence thesis by TARSKI:1;
end;

definition
  let X be set, R be Relation;
  func R Maximal_in X -> Subset of X means
  :Def1:
  for x being set holds x in it iff x is_maximal_wrt X, R;
  existence
  proof
    defpred P[set] means $1 is_maximal_wrt X, R;
    consider I being set such that
A1: for x being set holds x in I iff x in X & P[x] from XBOOLE_0:sch 1;
    for x being set 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 set;
    thus x in I implies x is_maximal_wrt X, R by A1;
    assume
A2: x is_maximal_wrt X, R;
    then x in X by WAYBEL_4:def 23;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    defpred P[set] means $1 is_maximal_wrt X, R;
    thus for X1,X2 being Subset of X st (for y being set holds y in X1 iff P[y
    ]) & (for y being set holds y in X2 iff P[y]) holds X1 = X2 from SubsetSEq;
  end;
end;

definition
  let x, X be set;
  pred x is_/\-irreducible_in X means
  :Def2:
  x in X & for z, y being 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;
  func /\-IRR X -> Subset of X means
  :Def3:
  for x being set holds x in it iff x is_/\-irreducible_in X;
  existence
  proof
    set irr = {z where z is Element of X : z is_/\-irreducible_in X };
    irr c= X
    proof
      let x be set;
      assume x in irr;
      then ex z being 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 being 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;
    then x in X by Def2;
    hence thesis by A1;
  end;
  uniqueness
  proof
    defpred P[set] means $1 is_/\-irreducible_in X;
    thus for X1,X2 being Subset of X st (for y being set holds y in X1 iff P[y
    ]) & (for y being set holds y in X2 iff P[y]) holds X1 = X2 from SubsetSEq;
  end;
end;

scheme
  FinIntersect {X() -> non empty finite set, P[set]} : for x being set st x in
  X() holds P[x]
provided
A1: for x being set st x is_/\-irreducible_in X() holds P[x] and
A2: for x, y being set st x in X() & y in X() & P[x] & P[y] holds P[x /\ y]
proof
  deffunc U(set) = {x where x is Element of X(): $1 c= x};
  given x being set such that
A3: x in X() and
A4: not P[x];
  defpred R[Nat] means ex s being Element of X() st card U(s) = $1 & not P[s];
  U(x) c= X()
  proof
    let x1 be set;
    assume x1 in U(x);
    then ex xx being Element of X() st x1 = xx & x c= xx;
    hence thesis;
  end;
  then reconsider Ux = U(x) as finite set;
A5: ex k being 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 being Nat such that
A6: R[k] and
A7: for n being Nat st R[n] holds k <= n from NAT_1:sch 5(A5);
  consider s being 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 set;
      assume x in U(s);
      then ex xx being Element of X() st x = xx & s c= xx;
      hence thesis;
    end;
    then reconsider Us = U(s) as finite set;
    consider z, y being 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,Def2;
A16: s c= y by A13,XBOOLE_1:17;
    U(z) c= X()
    proof
      let x be set;
      assume x in U(z);
      then ex xx being 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 set;
      assume x in U(y);
      then ex xx being 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 set;
      assume x in Uy;
      then consider xx being Element of X() such that
A19:  x = xx and
A20:  y c= xx;
      s c= xx by A16,A20,XBOOLE_1:1;
      hence thesis by A19;
    end;
    now
      assume s in Uy;
      then ex x being 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 set;
      assume x in Uz;
      then consider xx being Element of X() such that
A23:  x = xx and
A24:  z c= xx;
      s c= xx by A17,A24,XBOOLE_1:1;
      hence thesis by A23;
    end;
    now
      assume s in Uz;
      then ex x being 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 Th3:
  for X being non empty finite set, x being Element of X ex A being
  non empty Subset of X st x = meet A & for s being 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 being non empty Subset of X st $1 = meet S & for s
  being 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 being non empty Subset of X such that
A4: y = meet Sy and
A5: for s being set st s in Sy holds s is_/\-irreducible_in X by A3;
    consider Sx being non empty Subset of X such that
A6: x = meet Sx and
A7: for s being 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,Def2;
      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 being 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;
  attr B is (B1) means
  :Def4:
  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) by Def4;
    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 Th4:
  for X being set, B being non empty Subset-Family of X st B is
cap-closed for x being Element of B st x is_/\-irreducible_in B & x <> X for S
  being 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 being Element of B st x <> a & x <> b & x = a
  /\ b) or ex f being 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 being Element of B st x <> a & x <> b & x = a /\ b;
      hence P[A\/{s}];
    end;
    suppose
      ex f being Subset-Family of X st A = {} or A = f & Intersect f
      <> x & Intersect f in B;
      then consider f being 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,FINSUB_1:def 2;
              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,Def2,SETFAM_1:def 9;
end;

registration
  let X, D be non empty set, n be Element of NAT;
  cluster -> FinSequence-yielding for Function of X, n-tuples_on D;
  coherence
  proof
    let f be Function of X, n-tuples_on D;
    let x be set;
    assume x in dom f;
    then reconsider fx = f.x as Element of n-tuples_on D by FUNCT_2:5;
    thus thesis;
  end;
end;

registration
  let f be FinSequence-yielding Function, x be set;
  cluster f.x -> FinSequence-like;
  coherence
  proof
    per cases;
    suppose
      x in dom f;
      hence thesis by PRE_POLY:def 3;
    end;
    suppose
      not x in dom f;
      hence thesis by FUNCT_1:def 2;
    end;
  end;
end;

definition
  let n be Element of NAT, p, q be Tuple of n, BOOLEAN;
  func p '&' q -> Tuple of n, BOOLEAN means
  :Def5:
  for i being set st i in Seg n holds it.i = (p/.i) '&' (q/.i);
  existence
  proof
    deffunc F(set) = (p/.$1) '&' (q/.$1);
    consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j being 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 being set st i in Seg n holds it1.i = (p/.i) '&' (q/.i) and
A5: for i being 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 set;
      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 Th5:
  for n being Element of NAT, p being 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 set;
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 set;
    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
  for n being Element of NAT, p being 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 set;
    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 Th7:
  for n, i being Element of NAT st i < n holds (n-BinarySequence 2
to_power i).(i+1) = 1 & for j being 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 Element of NAT such that
A3: P[n];
    now
      assume
A4:   i < n+1;
      then
A5:   i <= n by NAT_1:13;
      per cases by A5,XXREAL_0:1;
      suppose
A6:     n = 0;
        0*n = n |-> 0 by EUCLID:def 4;
        then dom 0*n =Seg n by FUNCOP_1:13;
        then
A7:     len 0*n = n by FINSEQ_1:def 3;
        dom <*TRUE*> =Seg 1 by FINSEQ_1:38;
        then
A8:     1 in dom <*TRUE*> by FINSEQ_1:1;
A9:     i = 0 by A4,A6,NAT_1:13;
        hence B(n+1).(i+1) = (0*n^<*TRUE*>).(i+1) by A6,BINARI_3:28
          .= <*TRUE*>.1 by A6,A9,A7,A8,FINSEQ_1:def 7
          .= TRUE by FINSEQ_1:40;
      end;
      suppose
A10:    n > 0 & n = i;
        0*n = n |-> 0 by EUCLID:def 4;
        then dom 0*n = Seg n by FUNCOP_1:13;
        then
A11:    len 0*n = n by FINSEQ_1:def 3;
        dom <*TRUE*> = Seg 1 by FINSEQ_1:38;
        then
A12:    1 in dom <*TRUE*> by FINSEQ_1:1;
        thus B(n+1).(i+1) = (0*n^<*TRUE*>).(i+1) by A10,BINARI_3:28
          .= <*TRUE*>.1 by A10,A11,A12,FINSEQ_1:def 7
          .= TRUE by FINSEQ_1:40;
      end;
      suppose
A13:    n > 0 & n > i;
        then reconsider n9 = n as non empty Element of NAT;
A14:    0+1 <= i+1 by XREAL_1:6;
        i+1 <= n by A13,NAT_1:13;
        then i+1 in Seg n by A14,FINSEQ_1:1;
        then
A15:    i+1 in dom B(n) by Lm1;
        2 to_power i < 2 to_power n by A13,POWER:39;
        hence B(n+1).(i+1) = (B(n9)^<*FALSE*>).(i+1) by BINARI_3:27
          .= TRUE by A3,A13,A15,FINSEQ_1:def 7;
      end;
    end;
    hence P[n+1];
  end;
A16: P[ 0 ];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A16,A2);
  hence B.(i+1) = 1 by A1;
  defpred P[Element of NAT] means i < $1 implies for j being Element of NAT st
  i+1 <=j & j <= $1 holds B($1).(j+1)= FALSE;
  let j be Element of NAT such that
A17: j in Seg n and
A18: j<>i+1;
A19: 1 <= j by A17,FINSEQ_1:1;
A20: now
    let n be Element of NAT such that
A21: P[n];
    now
      assume i < n+1;
      then
A22:  i <= n by NAT_1:13;
A23:  0+1 <= i+1 by XREAL_1:6;
      let j be Element of NAT such that
A24:  i+1 <=j and
A25:  j <= n+1;
      per cases by A22,XXREAL_0:1;
      suppose
A26:    n = 0;
        1 <= j by A24,A23,XXREAL_0:2;
        then
A27:    j = 1 by A25,A26,XXREAL_0:1;
        dom B(n+1) = Seg (n+1) by Lm1;
        then not j+1 in dom B(n+1) by A26,A27,FINSEQ_1:1;
        hence B(n+1).(j+1) = FALSE by FUNCT_1:def 2;
      end;
      suppose
A28:    n > 0 & n = i;
A29:    dom B(n+1) = Seg (n+1) by Lm1;
        j+1 > n+1 by A24,A28,NAT_1:13;
        then not j+1 in dom B(n+1) by A29,FINSEQ_1:1;
        hence B(n+1).(j+1) = FALSE by FUNCT_1:def 2;
      end;
      suppose
A30:    n > 0 & n > i;
        then reconsider n9 = n as non empty Element of NAT;
A31:    2 to_power i < 2 to_power n by A30,POWER:39;
        thus B(n+1).(j+1) = FALSE
        proof
          j<n+1 or j=n+1 by A25,XXREAL_0:1;
          then
A32:      j <= n or j = n+1 by NAT_1:13;
          per cases by A32,XXREAL_0:1;
          suppose
            j = n+1;
            then
A33:        j+1 > n+1 by NAT_1:13;
            dom B(n+1) = Seg (n+1) by Lm1;
            then not j+1 in dom B(n+1) by A33,FINSEQ_1:1;
            hence thesis by FUNCT_1:def 2;
          end;
          suppose
A34:        j = n;
            dom B(n) = Seg n by Lm1;
            then
A35:        j = len B(n) by A34,FINSEQ_1:def 3;
            dom <*FALSE*> = Seg 1 by FINSEQ_1:38;
            then
A36:        1 in dom <*FALSE*> by FINSEQ_1:1;
            thus B(n+1).(j+1) = (B(n9)^<*FALSE*>).(j+1) by A31,BINARI_3:27
              .= <*FALSE*>.1 by A35,A36,FINSEQ_1:def 7
              .= FALSE by FINSEQ_1:40;
          end;
          suppose
A37:        j < n;
A38:        1 <= j+1 by NAT_1:12;
            j+1 <= n by A37,NAT_1:13;
            then j+1 in Seg n by A38,FINSEQ_1:1;
            then
A39:        j+1 in dom B(n) by Lm1;
            thus B(n+1).(j+1) = (B(n9)^<*FALSE*>).(j+1) by A31,BINARI_3:27
              .= B(n).(j+1) by A39,FINSEQ_1:def 7
              .= FALSE by A21,A24,A30,A37;
          end;
        end;
      end;
    end;
    hence P[n+1];
  end;
A40: P[ 0 ];
A41: for n being Element of NAT holds P[n] from NAT_1:sch 1(A40,A20);
  defpred P[Element of NAT] means i < $1 implies for j being Element of NAT st
  1 <=j & j < i+1 holds B($1).j = FALSE;
A42: now
    let n be Element of NAT such that
A43: P[n];
    now
      assume
A44:  i < n+1;
      then
A45:  i <= n by NAT_1:13;
      let j be Element of NAT such that
A46:  1 <=j and
A47:  j < i+1;
      per cases by A45,XXREAL_0:1;
      suppose
        n = 0;
        then i = 0 by A44,NAT_1:13;
        hence B(n+1).j = FALSE by A46,A47;
      end;
      suppose
A48:    n > 0 & i < n;
        then reconsider n9 = n as non empty Element of NAT;
A49:    dom B(n) = Seg n by Lm1;
A50:    i <= n by A44,NAT_1:13;
        j <= i by A47,NAT_1:13;
        then j <= n by A50,XXREAL_0:2;
        then
A51:    j in dom B(n) by A46,A49,FINSEQ_1:1;
        2 to_power i < 2 to_power n by A48,POWER:39;
        hence B(n+1).j = (B(n9)^<*FALSE*>).j by BINARI_3:27
          .= B(n).j by A51,FINSEQ_1:def 7
          .= FALSE by A43,A46,A47,A48;
      end;
      suppose
A52:    n > 0 & i = n;
        then j <= n by A47,NAT_1:13;
        then
A53:    j in Seg n by A46,FINSEQ_1:1;
A54:    0*n = n |-> 0 by EUCLID:def 4;
        then
A55:    j in dom 0*n by A53,FUNCOP_1:13;
        thus B(n+1).j = (0*n^<*TRUE*>).j by A52,BINARI_3:28
          .= (0*n).j by A55,FINSEQ_1:def 7
          .= FALSE by A54;
      end;
    end;
    hence P[n+1];
  end;
A56: P[ 0 ];
A57: for n being Element of NAT holds P[n] from NAT_1:sch 1(A56,A42);
A58: j <= n by A17,FINSEQ_1:1;
  per cases by A18,A58,XXREAL_0:1;
  suppose
    j < i+1;
    hence thesis by A1,A57,A19;
  end;
  suppose
A59: j > i+1 & j < n;
    then consider k being Nat such that
A60: j = k+1 by NAT_1:6;
    reconsider k as Element of NAT by ORDINAL1:def 12;
A61: k <= n by A59,A60,NAT_1:13;
    i+1 <= k by A59,A60,NAT_1:13;
    hence thesis by A1,A41,A60,A61;
  end;
  suppose
A62: j > i+1 & j = n;
    then consider m being Nat such that
A63: n = m+1 by NAT_1:6;
    reconsider m as Element of NAT by ORDINAL1:def 12;
    i < m by A62,A63,XREAL_1:6;
    then 2 to_power i < 2 to_power m by POWER:39;
    hence thesis by A62,A63,BINARI_3:26;
  end;
end;

begin :: 2. The relational model of data

definition
  struct DB-Rel (# Attributes -> finite non empty set, Domains -> non-empty
ManySortedSet of the Attributes, Relationship -> Subset of product the Domains
  #);
end;

begin :: 3. Dependency structures

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 by XBOOLE_1:2;
    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;
  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;
  redefine mode Element of F -> Dependency of X;
  correctness
  proof
    let x be Element of F;
    thus thesis;
  end;
end;

theorem Th8:
  for X, x being set holds x in Dependencies X iff ex a, b being
  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 being set 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 being Subset of X such that
A3: x = [a,b];
  thus thesis by A3,ZFMISC_1:87;
end;

theorem Th9:
  for X, x being set, F being Dependency-set of X holds x in F
  implies ex a, b being 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 being set 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;
  pred A >|> B, R means
  :Def7:
  for f, g being 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;
  func Dependency-str R -> Dependency-set of the Attributes of R equals
  { [A,
  B] where A, B is Subset of the Attributes of R: A >|> B, R };
  coherence
  proof
    set at = the Attributes of R;
    set X = {[A,B] where A,B is Subset of the Attributes of R: A >|> B, R};
    X c= [:bool at, bool at:]
    proof
      let x be set;
      assume x in X;
      then ex A, B being Subset of at st x = [A, B] & A >|> B, R;
      hence thesis by ZFMISC_1:def 2;
    end;
    hence thesis;
  end;
end;

theorem Th10:
  for R being DB-Rel, A, B being 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 being 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 :: 4. Full families of dependencies

definition
  let X be set, P, Q be Dependency of X;
  pred P >= Q means
  :Def9:
  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 Th11: :: antisymmetry
  for X being set, P, Q being 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,Def9;
A4: p`2 c= q`2 by A1,Def9;
  q`2 c= p`2 by A2,Def9;
  then
A5: p`2 = q`2 by A4,XBOOLE_0:def 10;
  p`1 c= q`1 by A2,Def9;
  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 Th12: :: transitivity
  for X being set, P, Q, S being 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,Def9;
  p`2 c= q`2 by A1,Def9;
  then
A4: p`2 c= r`2 by A3,XBOOLE_1:1;
A5: r`1 c= q`1 by A2,Def9;
  q`1 c= p`1 by A1,Def9;
  then r`1 c= p`1 by A5,XBOOLE_1:1;
  hence thesis by A4,Def9;
end;

definition
  let X be set, A, B be Subset of X;
  redefine func [A, B] -> Dependency of X;
  coherence by ZFMISC_1:def 2;
end;

theorem Th13:
  for X being set, A, B, A9, B9 being Subset of X holds [A,B] >= [
  A9,B9] iff A c= A9 & B9 c= B
proof
  let X be set, A, B, A9, B9 be Subset of X;
A1: [A,B]`2 = B;
A2: [A9,B9]`1 = A9;
A3: [A9,B9]`2 = B9;
  [A,B]`1 = A;
  hence thesis by A1,A2,A3,Def9;
end;

definition
  let X be set;
  func Dependencies-Order X -> Relation of Dependencies X equals
  { [P, Q]
  where P, Q is Dependency of X : P <= Q };
  coherence
  proof
    set Y = { [E, F] where E, F is Dependency of X : E <= F };
    Y c= [: Dependencies X, Dependencies X :]
    proof
      let x be set;
      assume x in Y;
      then ex E, F being Dependency of X st x = [E, F] & E <= F;
      hence thesis by ZFMISC_1:def 2;
    end;
    hence thesis;
  end;
end;

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

theorem Th15:
  for X being set holds dom Dependencies-Order X = [: bool X, bool X :]
proof
  let X be set;
  now
    let x be set;
    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:1;
end;

theorem Th16:
  for X being set holds rng Dependencies-Order X = [: bool X, bool X :]
proof
  let X be set;
  now
    let x be set;
    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:1;
end;

theorem Th17:
  for X being 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 set;
      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
    proof
      let x be set;
      assume x in dx;
      then reconsider x9 = x as Element of dx;
      x9 <= x9;
      hence thesis;
    end;
    hence dox is reflexive by A2,RELAT_2:def 9;
    dox is_antisymmetric_in dx
    proof
      let x, y be set;
      assume that
      x in dx and
      y in dx and
A3:   [x,y] in dox and
A4:   [y,x] in dox;
      consider x9, y9 being 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 being 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,RELAT_2:def 12;
    dox is_transitive_in dx
    proof
      let x, y, z be set;
      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 being 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 being 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,RELAT_2:def 16;
  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;
  attr F is (F1) means
  : Def11:
  for A being 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 Th18:
  for X being set, F being Dependency-set of X holds F is (F2) iff
  for A, B, C being 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 by RELAT_2:def 16;
    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,RELAT_2:def 8;
  end;
  assume
A6: for A,B,C being Subset of X st [A, B] in F & [B, C] in F holds [A, C
  ] in F;
  let x, y, z be set 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;
  attr F is (F3) means
  : Def12:
  for A, B, A9, B9 being Subset of X st [A, B]
  in F & [A, B] >= [A9, B9] holds [A9, B9] in F;
  attr F is (F4) means
  : Def13:
  for A, B, A9, B9 being Subset of X st [A, B]
  in F & [A9, B9] in F holds [A\/A9, B\/B9] in F;
end;

theorem Th19:
  for X being set holds Dependencies X is (F1) (F2) (F3) (F4)
proof
  let X be set;
  set D = Dependencies X;
  thus D is (F1)
  proof
    let A be Subset of X;
    thus thesis;
  end;
  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 set;
    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)
  proof
    let A, B, A9, B9 be Subset of X;
    thus thesis;
  end;
  thus D is (F4)
  proof
    let A, B, A9, B9 being Subset of X;
    thus thesis;
  end;
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;
  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 by Def14;
  end;
end;

definition
  let X be set;
  mode Full-family of X is full_family Dependency-set of X;
end;

theorem
  for X being finite set, F being 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 by Def14;
  cluster (F1) (F2) (F3) (F4) -> full_family for Dependency-set of X;
  correctness by Def14;
end;

definition
  let X be set, F be Dependency-set of X;
  attr F is (DC3) means
  :Def15:
  for A, B being 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 being Subset of X;
    assume B c= A;
    then
A2: [A, A] >= [A, B] by Th13;
    [A, A] in F by A1,Def11;
    hence thesis by A1,A2,Def12;
  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)
    proof
      let A be Subset of X;
      thus thesis by A3,Def15;
    end;
    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 by Th13;
    then [A9, A] in F by A3,Def15;
    then
A6: [A9, B] in F by A3,A4,Th18;
    B9 c= B by A5,Th13;
    then [B, B9] in F by A3,Def15;
    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 ::  F13_2_1_3:
  for X being set, F being Dependency-set of X st F is (DC3) (F2) holds
  F is (F1) (F3);

theorem ::  F1_3_13:
  for X being set, F being 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 by Def11;
end;

theorem Th23: ::  WWA1:
  for R being 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 being 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 being Element of R;
      assume f|A = g|A;
      then f|B = g|B by A5,Def7;
      hence thesis by A4,Def7;
    end;
    hence [A, C] in S;
  end;
  then
A6: S is (F2) by Th18;
A7: S is (DC3)
  proof
    let A, B being Subset of T such that
A8: B c= A;
    A >|> B, D
    proof
      let f, g being 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) by A6;
  thus S is (F2) by A1,Th18;
  thus S is (F3) by A7,A6;
  thus S is (F4)
  proof
    let A, B, A9, B9 being 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,Def7;
      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,Def7;
      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 :: Ex1:
  for X being set, K being Subset of X holds { [A, B] where A, B is
  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 is Subset of X : K c= A or B c= A };
  F c= [:bool X, bool X:]
  proof
    let x be set;
    assume x in F;
    then ex A, B being 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 being 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 being 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,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 being 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 being 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,XBOOLE_1:1;
    hence [A, C] in F by A15,A19;
  end;
  then
A20: F is (F2) by Th18;
  F is (DC3)
  proof
    let A, B be Subset of X;
    assume B c= A;
    hence thesis;
  end;
  hence thesis by A20,A1;
end;

begin :: 5. Maximal elements of full families

definition
  let X be set, F be Dependency-set of X;
  func Maximal_wrt F -> Dependency-set of X equals
  Dependencies-Order X
  Maximal_in F;
  coherence by RELSET_1:1;
end;

theorem
  for X being set, F being 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;
  pred x ^|^ y, F means
  :Def17:
  [x, y] in Maximal_wrt F;
end;

theorem Th26:
  for X being finite set, P being Dependency of X, F being
  Dependency-set of X st P in F ex A, B being 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 is 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 set;
    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 being Element of S such that
A4: m is_maximal_wrt S, DOX by A3,Th2;
  m in S by A4,WAYBEL_4:def 23;
  then
A5: ex y being Element of FF st m = y & x <= y;
  then consider a, b being 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 being set such that
A7: y in F and
A8: y <> m and
A9: [m, y] in DOX;
    consider e, f being 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,WAYBEL_4:def 23;
  end;
  hence [a,b] in Maximal_wrt F by A6,Def1;
  thus thesis by A5,A6;
end;

theorem Th27:
  for X being set, F being Dependency-set of X, A, B being Subset
of X holds A ^|^ B, F iff [A, B] in F & not ex A9, B9 being 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 by Def17;
    hence [x, y] in F;
A2: [x, y] is_maximal_wrt F, DOX by A1,Def1;
    given x9, y9 being 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,WAYBEL_4:def 23;
  end;
  assume that
A7: [x, y] in F and
A8: not ex x9, y9 being 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 being set such that
A9: z in F and
A10: z <> [x,y] and
A11: [[x, y],z] in DOX;
    consider x9,y9 being set 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 being 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 by Def17;
end;

definition
  let X be set, M be Dependency-set of X;
  attr M is (M1) means
  : Def18:
  for A being Subset of X ex A9, B9 being Subset
  of X st [A9, B9] >= [A, A] & [A9, B9] in M;
  attr M is (M2) means
  : Def19:
  for A, B, A9, B9 being Subset of X st [A, B]
  in M & [A9, B9] in M & [A, B] >= [A9, B9] holds A = A9 & B = B9;
  attr M is (M3) means
  : Def20:
  for A, B, A9, B9 being Subset of X st [A, B]
  in M & [A9, B9] in M & A9 c= B holds B9 c= B;
end;

theorem Th28: ::  WWA2:
  for X being finite non empty set, F being 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[set] means ex y being Dependency of X st $1 = y & y >= [A,A];
    consider MA being set such that
A2: for x being set holds x in MA iff x in F & P[x] from XBOOLE_0:sch
    1;
    MA c= F
    proof
      let x be set;
      assume x in MA;
      hence thesis by A2;
    end;
    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 being Element of MA such that
A4: x is_maximal_wrt MA, DOX by A3,Th2;
A5: x in MA by A4,WAYBEL_4:def 23;
    then x in F by A2;
    then consider A9, B9 being set 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 being 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 being set such that
A10:  z in F and
A11:  z <> x and
A12:  [x, z] in DOX;
      consider e, f being 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,WAYBEL_4:def 23;
    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,WAYBEL_4:def 23;
  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,Def17;
    [A9,B9] >= [B,B9] by A23,Th13;
    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] by Th13;
    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 Th29: :: WWA2a check this proof, WWA is sketchy
  for X being finite set, M, F being Dependency-set of X st M is
(M1) (M2) (M3) & F = {[A, B] where A, B is Subset of X : ex A9, B9 being Subset
  of X st [A9, B9] >= [A, B] & [A9, B9] in M} holds M = Maximal_wrt F & F is
  full_family & for G being 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 is Subset of X: ex A9, B9 being 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 being Subset of X st [A9, B9] >= [A, A] & [A9, B9] in M
    by A1,Def18;
    hence thesis by A2;
  end;
A4: now
    let x be set;
    assume x in F;
    then consider a, b being Subset of X such that
A5: x = [a,b] and
A6: ex a9, b9 being Subset of X st [a9, b9] >= [a, b] & [a9, b9] in M by A2;
    consider a9, b9 being 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 being 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 being Subset of X such that
A15: [A9, B9] >= [A, B] and
A16: [A9, B9] in M by A9,A13;
    consider B19, C9 being 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,Th13;
    B c= B9 by A15,Th13;
    then B19 c= B9 by A19,XBOOLE_1:1;
    then C9 c= B9 by A1,A16,A18,Def20;
    then
A20: [A9, B9] >= [A9, C9] by Th13;
A21: C c= C9 by A17,Th13;
    A9 c= A by A15,Th13;
    then [A9,C9] >= [A, C] by A21,Th13;
    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 being 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,Th13;
    consider a19,b19 being 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,Th13;
    consider A99, B99 being Subset of X such that
A32: [A99, B99] >= [A\/A9, A\/A9] and
A33: [A99, B99] in M by A1,Def18;
A34: A\/A9 c= B99 by A32,Th13;
    a19 c= A9 by A29,Th13;
    then a19 c= A\/A9 by XBOOLE_1:10;
    then a19 c= B99 by A34,XBOOLE_1:1;
    then b19 c= B99 by A1,A33,A30,Def20;
    then
A35: B9 c= B99 by A31,XBOOLE_1:1;
    a1 c= A by A26,Th13;
    then a1 c= A\/A9 by XBOOLE_1:10;
    then a1 c= B99 by A34,XBOOLE_1:1;
    then b1 c= B99 by A1,A33,A27,Def20;
    then B c= B99 by A28,XBOOLE_1:1;
    then
A36: B\/B9 c= B99\/B99 by A35,XBOOLE_1:13;
    A99 c= A\/A9 by A32,Th13;
    then [A99,B99] >= [A\/A9,B\/B9] by A36,Th13;
    hence thesis by A2,A33;
  end;
  set DOX = Dependencies-Order X;
  now
    let x be set;
    hereby
      assume
A37:  x in M;
      then consider a, b being 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 being set such that
A39:    y in F and
A40:    y <> x and
A41:    [x, y] in DOX;
        consider e, f being 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 being 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,Def19;
        c9 = a by A1,A37,A38,A47,A49,Def19;
        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 being 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,WAYBEL_4:def 23;
  end;
  hence M = Maximal_wrt F by TARSKI:1;
  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 being 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 being Full-family of X such that
A62: M = Maximal_wrt G;
  now
    let x be set;
    hereby
A63:  field DOX = [:bool X, bool X:] by Th17;
      assume
A64:  x in G;
      then consider a, b being Subset of X such that
A65:  x = [a,b] by Th9;
      defpred P[set] means ex y being Dependency of X st $1 = y & y >= [a,b];
      consider MA being set such that
A66:  for x being set holds x in MA iff x in G & P[x] from XBOOLE_0:
      sch 1;
      MA c= G
      proof
        let x be set;
        assume x in MA;
        hence thesis by A66;
      end;
      then
A67:  MA is finite Subset of field DOX by A63,XBOOLE_1:1;
      MA <> {} by A64,A65,A66;
      then consider m being Element of MA such that
A68:  m is_maximal_wrt MA, DOX by A67,Th2;
A69:  m in MA by A68,WAYBEL_4:def 23;
      then m in G by A66;
      then
A70:  ex a9, b9 being Subset of X st m = [a9,b9] by Th9;
      m is_maximal_wrt G, DOX
      proof
A71:    ex mm being Dependency of X st m = mm & mm >= [a,b] by A66,A69;
        thus m in G by A66,A69;
        given y being set such that
A72:    y in G and
A73:    y <> m and
A74:    [m, y] in DOX;
        consider e, f being 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,WAYBEL_4:def 23;
      end;
      then
A78:  m in (DOX Maximal_in G) by Def1;
      ex y being 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 being 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:1;
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 being Subset of X st [A9, B9]>=[[#]X, [#]X]&[A9, B9] in M by Def18
;
    hence thesis;
  end;
end;

theorem Th30: ::  Ex2:
  for X being finite set, F being Dependency-set of X, K being
  Subset of X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A }
  holds {[K, X]}\/{[A, A] where A is 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 is 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 is Subset of X : not K c= a};
    {[a, a] where a is 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 set;
    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 is Subset of X : not K c= A};
      then ex A being 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 is Subset of X : not K c= a};
      then consider a being 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 is Subset of X : ex A9, B9 being Subset of X st
  [A9, B9] >= [A, B] & [A9, B9] in M};
A11: FF c= [:bool X, bool X:]
  proof
    let x be set;
    assume x in FF;
    then ex A, B being Subset of X st x = [A,B] & ex A9, B9 being 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,Th13;
A17: B9 c= B by A15,Th13;
    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 is Subset of X : K c= A or B c= A };
A21: now
    let x be set;
    hereby
A22:  {[a, a] where a is 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 being 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] by Th13;
        hence x in FF by A25,A24,A23;
      end;
      suppose
A27:    not K c= A;
        then
A28:    [A,A] in {[a, a] where a is Subset of X : not K c= a};
        [A,A] >= [A,B] by A26,A27,Th13;
        hence x in FF by A25,A22,A28;
      end;
    end;
    assume x in FF;
    then consider A, B being Subset of X such that
A29: x = [A,B] and
A30: ex A9, B9 being Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M;
    consider A9, B9 being 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,Th13;
      hence x in F by A20,A29;
    end;
    suppose
      [A9,B9] in {[a, a] where a is Subset of X : not K c= a};
      then consider a being 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,Th13;
      A9 c= A by A31,Th13;
      then B c= A by A34,A35,A36,XBOOLE_1:1;
      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,Th13;
      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:1;
end;

begin :: 6. Saturated subsets of Attributes

definition
  let X be set, F be Dependency-set of X;
  func saturated-subsets F -> Subset-Family of X equals
  { B where B is Subset
  of X: ex A being Subset of X st A ^|^ B, F };
  coherence
  proof
    set SS = {B where B is Subset of X: ex A being Subset of X st A ^|^B,F};
    SS c= bool X
    proof
      let x be set;
      assume x in SS;
      then
      ex B being Subset of X st x = B & ex A being 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[set,set] means ex a,b being set st $1 = [a,b] & $2 = [a,b]`2;
    set ss = {B where B is Subset of X: ex A being Subset of X st A ^|^ B, F };
A1: for x being set st x in F ex y being set st P[x,y]
    proof
      let x be set;
      assume x in F;
      then consider a, b being 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 being Function such that
A3: dom f = F and
A4: for x being set st x in F holds P[x,f.x] from CLASSES1:sch 1(A1);
A5: ss c= rng f
    proof
      let x be set;
      assume x in ss;
      then consider B being Subset of X such that
A6:   x = B and
A7:   ex A being Subset of X st A ^|^ B, F;
      consider A being Subset of X such that
A8:   A ^|^ B, F by A7;
A9:   [A, B] in Maximal_wrt F by A8,Def17;
      then
A10:    ex a,b being set st [A,B] = [a,b] & f.[A,B] = [a,b]`2 by A4;
      [A,B]`2 = B;
      then 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 Th31:
  for X, x being set, F being Dependency-set of X holds x in
  saturated-subsets F iff ex B, A being 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 being Subset of X such that
A1: x = B and
A2: ex A being Subset of X st A^|^B,F;
    consider A being 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 being Subset of X such that
A4: x = B and
A5: A ^|^ B, F;
  thus thesis by A4,A5;
end;

theorem Th32: ::  WWA3:
  for X being finite non empty set, F being 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 being Subset of X such that
A2: [A9,B9] >= [[#]X,[#]X] and
A3: [A9,B9] in Maximal_wrt F by Def18;
  [#]X c= B9 by A2,Th13;
  then
A4: [#]X = B9 by XBOOLE_0:def 10;
  A9 ^|^ B9, F by A3,Def17;
  then X in ss by A4;
  hence ss is (B1) by Def4;
  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 being 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,Def17;
    consider B1, A1 being 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,Def17;
    consider A9, B9 being Subset of X such that
A14: [A9,B9] >= [a9/\b9,a9/\b9] and
A15: [A9,B9] in Maximal_wrt F by A1,Def18;
A16: A9 c= a/\b by A14,Th13;
    a/\b c= b by XBOOLE_1:17;
    then A9 c= B2 by A8,A16,XBOOLE_1:1;
    then
A17: B9 c= B2 by A10,A15,A7,Def20;
A18: a/\b c= B9 by A14,Th13;
    a/\b c= a by XBOOLE_1:17;
    then A9 c= B1 by A11,A16,XBOOLE_1:1;
    then B9 c= B1 by A13,A15,A7,Def20;
    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,Def17;
    hence thesis by A19;
  end;
end;

definition
  let X be set, B be set;
  func X deps_encl_by B -> Dependency-set of X equals
  { [a, b] where a, b is
  Subset of X : for c being set st c in B & a c= c holds b c= c};
  coherence
  proof
    set F = {[a, b] where a,b is Subset of X : for c being set st c in B & a
    c= c holds b c= c};
    F c= [:bool X, bool X:]
    proof
      let x be set;
      assume x in F;
      then
      ex a, b being Subset of X st x = [a,b] & for c being set st c in B &
      a c= c holds b c= c;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem Th33: ::  WWA3_0:
  for X being set, B being Subset-Family of X, F being
  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 set;
      thus x in F implies x in Dependencies X;
      assume x in Dependencies X;
      then consider x1, x2 being set such that
A2:   x1 in bool X and
A3:   x2 in bool X and
A4:   x = [x1, x2] by ZFMISC_1:def 2;
      for g being 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:1;
    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 being 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 being Subset of X such that
A8:   [x,y] = [a,b] and
A9:   for c being 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,Th13;
A18:  a c= a9 by A16,Th13;
      now
        let c be set;
        assume that
A19:    c in B and
A20:    a9 c= c;
        a c= c by A18,A20,XBOOLE_1:1;
        then b c= c by A5,A15,A19;
        hence b9 c= c by A17,XBOOLE_1:1;
      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 Th34: ::  WWA3_00:
  for X being finite non empty set, B being 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 set;
  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 being Subset of X such that
A2: [a9,b9] >= [x99,x99] and
A3: [a9, b9] in M by Def18;
A4: a9 c= x99 by A2,Th13;
  [a9,b9] in F by A3;
  then consider a, b being Subset of X such that
A5: [a9,b9] = [a,b] and
A6: for c being set st c in B & a c= c holds b c= c;
A7: a ^|^ b, F by A3,A5,Def17;
  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,Th13;
  then b = x by A9,A8,XBOOLE_0:def 10;
  hence thesis by A7;
end;

theorem Th35: ::  WWA3a:
  for X being finite non empty set, B being Subset-Family of X st
  B is (B1) (B2) holds B = saturated-subsets (X deps_encl_by B) & for G being
  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 by Def4;
A2: X in B by A1,Def4;
  now
    let x be set;
    B c= ss by Th34;
    hence x in B implies x in ss;
    assume x in ss;
    then consider b, a being Subset of X such that
A3: x = b and
A4: a ^|^ b, F by Th31;
    [a,b] in M by A4,Def17;
    then [a,b] in F;
    then consider aa, bb being Subset of X such that
A5: [a, b] = [aa, bb] and
A6: for c being 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 is Element of B9: a c= b9 };
A8: S c= bool X
    proof
      let x be set;
      assume x in S;
      then consider b9 being 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 set;
      assume x in S;
      then ex b9 being 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 set;
      assume
A14:  x in b;
      now
        let Y be set;
        assume Y in S;
        then consider b9 being 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,Th13;
      hence contradiction by A4,A20,A19,Th27;
    end;
    hence x in B by A1,A2,A3,A10,Th1;
  end;
  hence B = saturated-subsets F by TARSKI:1;
  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 set;
    hereby
      assume x in G;
      then reconsider x1 = x as Element of G;
      reconsider x9 = x1 as Dependency of X;
      consider a, b being Subset of X such that
A23:  x9 = [a,b] by Th8;
      now
        consider a99, b99 being Subset of X such that
A24:    [a99,b99] in MG and
A25:    [a99, b99] >= x9 by Th26;
A26:    b c= b99 by A23,A25,Th13;
        let b9 be set such that
A27:    b9 in B9 and
A28:    a c= b9;
        consider b19, a9 being Subset of X such that
A29:    b9 = b19 and
A30:    a9 ^|^ b19, G by A21,A27,Th31;
        a99 c= a by A23,A25,Th13;
        then
A31:    a99 c= b9 by A28,XBOOLE_1:1;
        [a9,b9] in MG by A29,A30,Def17;
        then b99 c= b19 by A22,A29,A24,A31,Def20;
        hence b c= b9 by A29,A26,XBOOLE_1:1;
      end;
      hence x in F by A23;
    end;
    assume x in F;
    then consider a, b being Subset of X such that
A32: x = [a,b] and
A33: for c being set st c in B & a c= c holds b c= c;
    consider a9, b9 being Subset of X such that
A34: [a9, b9] >= [a,a] and
A35: [a9, b9] in MG by A22,Def18;
A36: a9 c= a by A34,Th13;
    a9 ^|^ b9, G by A35,Def17;
    then
A37: b9 in B by A21;
    a c= b9 by A34,Th13;
    then b c= b9 by A33,A37;
    then [a9,b9] >= [a,b] by A36,Th13;
    hence x in G by A32,A35,Def12;
  end;
  hence thesis by TARSKI:1;
end;

definition
  let X be set, F be Dependency-set of X;
  func enclosure_of F -> Subset-Family of X equals
  { b where b is Subset of X
  : for A, B being Subset of X st [A, B] in F & A c= b holds B c= b };
  coherence
  proof
    set B = { b where b is Subset of X : for x, y being Subset of X st [x, y]
    in F & x c= b holds y c= b};
    B c= bool X
    proof
      let z be set;
      assume z in B;
      then
      ex b being Subset of X st z = b & for x, y being Subset of X st [x,
      y] in F & x c= b holds y c= b;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem Th36: ::  WWA3c:
  for X being finite non empty set, F being 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 being 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) by Def4;
  let a, b be set such that
A2: a in B and
A3: b in B;
  consider b9 being Subset of X such that
A4: b9 = b and
A5: for x, y being Subset of X st [x, y] in F & x c= b9 holds y c= b9 by A3;
  consider a9 being Subset of X such that
A6: a9 = a and
A7: for x, y being 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 Th37: :: WWA3b
:: Added for proving WWA7 where it is referenced but never
:: stated.  This characterizes the smallest full family
:: containing a given dependency set
  for X being finite non empty set, F being Dependency-set of X
holds F c= X deps_encl_by enclosure_of F & for G being 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 set;
    assume
A1: x in F;
    then consider a, b being 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 being Subset of X st c9 = c & for x, y being 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 set;
  set GG = {[e, f] where e, f is Subset of X : for c being 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 being Subset of X such that
A10: z = [a,b] and
A11: for c being 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 set 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 being 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 being Subset of X such that
A18: [x,y] = [e,f] and
A19: for c being 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;
  func Dependency-closure F -> Full-family of X means
  :Def24:
  F c= it & for G
  being Dependency-set of X st F c= G & G is full_family holds it c= G;
  existence
  proof
    set B = {c where c is Subset of X : for x, y being 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 set;
      assume x in B;
      then
      ex c being Subset of X st x = c & for x, y being 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 being 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 being 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 Th38: ::  WWA3d:
  for X being finite non empty set, F being 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 being 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 Th39: ::  Ex3:
  for X being set, K being Subset of X, B being Subset-Family of X
  st B = {X}\/{A where A is 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 is 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) by Def4;
  set BB1 = {B where B is 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 being 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 :: Ex3a:
  for X being finite non empty set, F being Dependency-set of X, K being
  Subset of X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A }
  holds {X}\/{B where B is 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 being Subset of X;
  set BB = {X}\/{B where B is Subset of X : not K c= B};
  BB c= bool X
  proof
    let x be set;
    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 is Subset of X : not K c= B};
      then ex B being 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 is Subset of X : for c being 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 is Subset of X : K c= A or B c= A };
  now
    let x be set;
    hereby
      assume x in F;
      then consider a, b being 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 is Subset of X : not K c= B};
              then ex B being Subset of X st c = B & not K c= B;
              hence thesis by A9,A10,XBOOLE_1:1;
            end;
          end;
        end;
        suppose
          b c= a;
          hence b c= c by A9,XBOOLE_1:1;
        end;
      end;
      hence x in G by A6;
    end;
    assume x in G;
    then consider a, b being Subset of X such that
A11: x = [a,b] and
A12: for c being set st c in BB9 & a c= c holds b c= c;
    now
      assume not K c= a;
      then a in {B where B is 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:1;
  BB9 is (B1) by Th39;
  hence thesis by A4,A3,A13,Th35;
end;

theorem
  for X being finite set, F being Dependency-set of X, K being Subset of
X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A } holds {X}\/{B
  where B is Subset of X : not K c= B} = saturated-subsets F
proof
  let X be finite set, F be Dependency-set of X, K being Subset of X;
  set BB = {X}\/{B where B is Subset of X : not K c= B};
  set M = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A};
  set ss = saturated-subsets F;
  assume F = { [A, B] where A, B is 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 set;
    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,Def17;
        x = X by A4,TARSKI:def 1;
        hence x in ss by A2,A5;
      end;
      suppose
        x in {B where B is Subset of X : not K c= B};
        then consider B being Subset of X such that
A6:     x = B and
A7:     not K c= B;
        [B,B] in {[A, A] where A is 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,Def17;
        hence x in ss by A6;
      end;
    end;
    assume x in ss;
    then consider b, a being Subset of X such that
A8: x = b and
A9: a ^|^ b, F by Th31;
A10: [a,b] in M by A1,A9,Def17;
    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 is Subset of X : not K c= A};
      then consider c being Subset of X such that
A11:  [a,b] = [c,c] and
A12:  not K c= c;
A13:  c in {B where B is 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:1;
end;

definition
  let X, G be set, B be Subset-Family of X;
  pred G is_generator-set_of B means
  :Def25:
  G c= B & B = { Intersect S where S is Subset-Family of X: S c= G };
end;

theorem :: WWA4b:
  for X be finite non empty set, G being 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 is Subset-Family of X: S c= G };
    thus
A2: G c= ssF by Th34;
    now
      let x be set;
      hereby
        assume x in ssF;
        then consider b9, a9 being Subset of X such that
A3:     x = b9 and
A4:     a9 ^|^ b9, F by Th31;
        [a9, b9] in Maximal_wrt F by A4,Def17;
        then [a9,b9] in F;
        then consider a, b being Subset of X such that
A5:     [a, b] = [a9, b9] and
A6:     for c being set st c in G & a c= c holds b c= c;
        set C = {c where c is Subset of X: c in G & a c= c};
        C c= bool X
        proof
          let x be set;
          assume x in C;
          then ex c being 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 being 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 set;
          assume c in C;
          then ex cc being 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,Th13;
            hence thesis by A4,A5,A8,A10,A13,Th27;
          end;
        end;
      end;
      assume x in H;
      then
A14:  ex S being Subset-Family of X st Intersect S = x & S c= G;
      X in ssF by A1,Def4;
      hence x in ssF by A1,A2,A14,Th1,XBOOLE_1:1;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th43: ::  WWA4a:
  for X being finite non empty set, F being Full-family of X ex G
  being 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 is Subset-Family of X: S c= G };
    thus G c= G;
    now
      let x be set;
      hereby
        set sx = {x};
        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 being Subset-Family of X st Intersect S = x & S c= G;
      X in G by A1,Def4;
      hence x in G by A1,A5,Th1;
    end;
    hence thesis by TARSKI:1;
  end;
  thus thesis by A1,Th35;
end;

:: WWA did not show what generators B are,
:: they are the irreducible elements \ X

theorem
  for X being set, B being 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 is Subset-Family of X:S c= G};
  thus G c= B;
A2: X in B by A1,Def4;
  now
    let x be set;
    hereby
      assume x in B;
      then reconsider xx = x as Element of B;
      consider yz being non empty Subset of B such that
A3:   xx = meet yz and
A4:   for s being 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;
A5:   yz c= G
      proof
        let x be set;
        assume x in yz;
        then x is_/\-irreducible_in B by A4;
        hence thesis by Def3;
      end;
      Intersect yz = meet yz by SETFAM_1:def 9;
      hence x in H by A3,A5;
    end;
    assume x in H;
    then ex S being Subset-Family of X st x = Intersect S & S c= G;
    hence x in B by A1,A2,Th1,XBOOLE_1:1;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  for X, G being set, B being 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 is Subset-Family of X: S c= G } by A2,Def25;
A4: G c= B by A2,Def25;
  let x be set;
  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 being 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 :: 7. Justification of the axioms

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
  for X being non empty finite set, F being Full-family of X ex R being
  DB-Rel st the Attributes of R = X & (for a being 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 being 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 being FinSequence such that
A2: rng H = G and
  H is one-to-one by FINSEQ_4:58;
A3: dom D = X by PARTFUN1:def 2;
A4: now
    set f = X --> 0;
    thus dom f = dom D by A3,FUNCOP_1:13;
    let x be set;
    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 set;
      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 being Element of X holds (the
    Domains of BD).a = INT by FUNCOP_1:7;
    set Ds = Dependency-str BD;
    now
      let x be set;
      hereby
        assume x in F;
        then consider A, B being Subset of X such that
A8:     x = [A, B] and
        for g being 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 being Subset of the Attributes of BD such that
A9:   x = [A,B] and
      A >|> B, BD;
      for g being 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:1;
  end;
  suppose
A10: G is non empty;
    then H is non empty by A2;
    then reconsider n =len H as non empty Element of NAT;
    defpred R[set,Element of n-tuples_on BOOLEAN ] means
     for i being 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 being Nat st i in Seg n ex x being 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 being FinSequence of BOOLEAN such that
A15:  dom y = Seg n and
A16:  for i being 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 is 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 being Function of X, n-tuples_on BOOLEAN such that
A18: for x being 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 is Element of product D : ex i being Element of NAT st
for x being 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 set;
      assume x in R;
      then ex f being Element of product D st x = f & ex i being Element of
NAT st for x being 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 by FUNCOP_1:7
        .= 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 being Element of X holds (the
    Domains of BD).a = INT by FUNCOP_1:7;
    set Ds = Dependency-str BD;
A21: dom H = Seg n by FINSEQ_1:def 3;
    now
      let x be set;
      hereby
        assume x in F;
        then consider A, B being Subset of X such that
A22:    x = [A, B] and
A23:    for g being 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 being Element of product D such that
A25:      f = Rf and
A26:      ex i being Element of NAT st for x being Element of X holds
          Rf.x = Absval ((n-BinarySequence i) '&' (M.x
           qua Element of n-tuples_on BOOLEAN));
          consider fi being Element of NAT such that
A27:      for x being 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 being Element of product D such that
A28:      g = Rg and
A29:      ex i being Element of NAT st for x being Element of X holds
          Rg.x = Absval ((n-BinarySequence i) '&' (M.x
           qua Element of n-tuples_on BOOLEAN));
          consider gi being Element of NAT such that
A30:      for x being 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 set 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 set;
              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 being set such that
A41:              xx in A and
A42:              not xx in H.i by A40,TARSKI:def 3;
                  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 being 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 being Function of X, NAT such that
A53:    for x being Element of X holds f.x = F(x) from FUNCT_2:sch 4;
A54:    now
          let x be set;
          assume x in dom D;
          then reconsider x9 = x as Element of X;
          f.x = Absval ((n-BinarySequence 0) '&' (M.x9
           qua Element of n-tuples_on BOOLEAN)) by A53;
          then f.x in NAT;
          then f.x9 in INT by NUMBERS:17;
          hence f.x in D.x by FUNCOP_1:7;
        end;
A55:    dom f = dom D by A3,FUNCT_2:def 1;
        then reconsider f as Element of product D by A54,CARD_3:def 5;
        consider i being 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 being Nat such that
A58:    i = k+1 by NAT_1:6;
        consider bx being set such that
A59:    bx in B and
A60:    not bx in gg by A52,TARSKI:def 3;
        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 being Function of X, NAT such that
A63:    for x being Element of X holds g.x = F(x) from FUNCT_2:sch 4;
A64:    now
          let x be set;
          assume x in dom D;
          then reconsider x9 = x as Element of X;
          g.x = Absval ((n-BinarySequence 2 to_power k) '&' (M.x9
           qua Element of n-tuples_on BOOLEAN)) by A63;
          then g.x in NAT;
          then g.x9 in INT by NUMBERS:17;
          hence g.x in D.x by FUNCOP_1:7;
        end;
A65:    dom g = dom D by A3,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 set;
          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 set;
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,Def7;
        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:1;
  end;
end;

begin :: 8. Structure of the family of candidate keys

Lm3: for X, F, BB being set st F = {[a, b] where a,b is Subset of X : for c
being set st c in BB & a c= c holds b c= c} for x, y being Subset of X holds [x
,y] in F iff for c being 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 is Subset of X : for c being 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 being Subset of X such that
A2: [x,y] = [a, b] and
A3: for c being 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 being set st c in BB & x c= c holds y c= c by A3,A4;
  end;
  assume for c being 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;
  func candidate-keys F -> Subset-Family of X equals
  { A where A is Subset of
X: [A, X] in Maximal_wrt F };
  coherence
  proof
    set B = {A where A is Subset of X : [A, X] in Maximal_wrt F};
    B c= bool X
    proof
      let x be set;
      assume x in B;
      then ex A being Subset of X st x = A & [A, X] in Maximal_wrt F;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem :: Ex8:
  for X being finite set, F being Dependency-set of X, K being Subset of
  X st F = { [A, B] where A, B is 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 is Subset of X : K c= A or B c= A };
  then
A1: Maximal_wrt F = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A}
  by Th30;
  now
    let x be set;
    hereby
      assume x in candidate-keys F;
      then consider a being 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 is Subset of X : not K c= A};
        then consider A being 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:1;
end;

notation
  let X be set;
  antonym X is (C1) for X is empty;
end;

definition
  let X be set;
  attr X is without_proper_subsets means
  :Def27:
  for x, y being 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 :: WWA6:
  for R being 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 by Def4;
  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,Def17;
  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 being Subset of X such that
A8: k2 = a2 and
A9: [a2, X] in Maximal_wrt F by A6;
  consider a1 being 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,Th13;
  hence thesis by A10,A11,A8,A9,A2,Def19;
end;

theorem :: WWA6a:
  for X being finite set, C being Subset-Family of X st C is (C1) (C2)
  ex F being 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 is Subset of X : for K being Subset of X st K in C holds
  not K c= b};
A1: [#]X = X;
  B c= bool X
  proof
    let x be set;
    assume x in B;
    then ex b being Subset of X st x = b & for K being 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 is Subset of X : for c being 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 being Subset of X st c = b & for K being 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 being 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,Th13;
    X c= b by A9,Th13;
    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,XBOOLE_1:1;
      then K = x9 by A3,A5,A13,Def27;
      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 set;
    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 being 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,Def17;
      given K being Subset of X such that
A20:  K in C and
A21:  K c= A;
A22:  [K, [#]X] >= [A, [#]X] by A21,Th13;
      [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 being 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 being Subset of X st b = X & for K being Subset of X st K in C
    holds not K c= b;
    then not ex K being set st K in C;
    hence contradiction by A2,XBOOLE_0:def 1;
  end;
  hence thesis by TARSKI:1;
end;

theorem :: WWA6a A more reasonable version
  for X being finite set, C being Subset-Family of X, B being set st C
is (C1) (C2) & B = {b where b is Subset of X : for K being 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 is Subset of X : for K being Subset of X st K in C
  holds not K c= b};
  B c= bool X
  proof
    let x be set;
    assume x in B;
    then ex b being Subset of X st x = b & for K being 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 being Subset of X st c = b & for K being 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 being 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,Th13;
    X c= b by A10,Th13;
    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,XBOOLE_1:1;
      then K = x9 by A2,A6,A14,Def27;
      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 set;
    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 being 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,Def17;
      given K being Subset of X such that
A21:  K in C and
A22:  K c= A;
A23:  [K, [#]X] >= [A, [#]X] by A22,Th13;
      [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 being 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 being Subset of X st b = X & for K being Subset of X st K in C
    holds not K c= b by A3;
    then not ex K being set st K in C;
    hence contradiction by A1,XBOOLE_0:def 1;
  end;
  hence thesis by TARSKI:1;
end;

theorem :: WWA6a proof II
  for X being non empty finite set, C being Subset-Family of X st C is
  (C1) (C2) ex R being 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 is Subset of X: for K being 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 is Subset of X : L in M0 };
A3: R c= product D
  proof
    let x be set;
A4: dom D = X by PARTFUN1:def 2;
    assume x in R;
    then consider L being 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 by FUNCOP_1:13;
A7: now
      let x be set 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 by A8,FUNCOP_1:7;
        hence g.x in D.x by A9;
      end;
    end;
    dom g = dom (X --> 0)\/L by A6,FUNCT_4:def 1
      .= X\/L by FUNCOP_1:13
      .= X by XBOOLE_1:12;
    hence thesis by A5,A4,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 is 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 being 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 by FUNCOP_1:13;
      g in R;
      then consider Lg being 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 by FUNCOP_1:13;
      per cases by A17,A21,TARSKI:def 1;
      suppose
        Lf in M & Lg in M;
        then ex Lff being Subset of X st Lf = Lff & for K being Subset of X
        st K in C holds Lff/\K <> {};
        then
A23:    Lf /\ A <> {} by A13;
        then consider a being set 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 by A24,FUNCOP_1:7;
          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 being Subset of X st Lf = L & for K being Subset of X st K
        in C holds L/\K <> {};
        then
A31:    Lf /\ A <> {} by A13;
        then consider a being set 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
          .= {} by A32,FUNCOP_1:7;
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 being Subset of X st Lg = L & for K being Subset of X st K
        in C holds L/\K <> {};
        then
A37:    Lg /\ A <> {} by A13;
        then consider a being set 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
          .= {} by A38,FUNCOP_1:7;
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 by Def7;
    then [A,X] in ds;
    then consider a, b being 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,Th13;
    [a,b] in ds by A42;
    then consider aa, XX being 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,Th13;
    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 by XBOOLE_1:2;
        then a = X by A11,SUBSET_1:19;
        hence contradiction by A44,A51,XBOOLE_0:def 10;
      end;
      then consider y being set 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,XBOOLE_1:1;
        then K = A by A2,A13,A54,Def27;
        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 by A53,FUNCT_1:49
        .= 0 by A53,FUNCOP_1:7;
A58:  dom (a` --> a`) = a` by FUNCOP_1:13;
      now
A59:    dom r1 = dom (X --> 0)\/dom (a` --> a`) by FUNCT_4:def 1
          .= X\/dom (a` --> a`) by FUNCOP_1:13
          .= X\/a` by FUNCOP_1:13
          .= X by XBOOLE_1:12;
        dom r0 = X by FUNCOP_1:13;
        hence dom (r0|a) = dom r1 /\ a by A59,RELAT_1:61;
        let x be set;
        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,Def7;
    end;
    then [A,X] in Maximal_wrt ds by A42,A49,XBOOLE_0:def 10;
    hence x in ck;
  end;
  now
    let x be set;
    thus x in C implies x in ck by A12;
    assume x in ck;
    then consider A being 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 being 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,Def17;
      let K be set such that
A71:  K in C and
A72:  K c= A;
      K in ck by A12,A71;
      then consider B being 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,Th13;
      hence contradiction by A73,A74,A75,A70,Th27;
    end;
    set m = { a where a is Element of X: not a in A & ex K being set st K in C
    & a in K };
A76: now
      let x be set;
      assume x in m;
      then ex a being Element of X st x = a & not a in A & ex K being set st
      K in C & a in K;
      hence x in X;
    end;
    consider K being set 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 being set such that
A80: k in K and
A81: not k in A by TARSKI:def 3;
    reconsider k as Element of X by A80;
A82: k in m by A77,A80,A81;
    then consider n being set 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 being set such that
A85:  k in K and
A86:  not k in A by TARSKI:def 3;
      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 by FUNCOP_1:13;
    now
A89:  dom r1 = dom (X --> 0)\/dom (m --> m) by FUNCT_4:def 1
        .= X\/dom (m --> m) by FUNCOP_1:13
        .= X\/m by FUNCOP_1:13
        .= X by XBOOLE_1:12;
      dom r0 = X by FUNCOP_1:13;
      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 set such that
A91:  x in dom (r0|A);
A92:  now
        assume x in m;
        then ex a being Element of X st x = a & not a in A & ex K being 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;
A95: m c= X;
    then (r0|X).n = r0.n by A83,FUNCT_1:49
      .= 0 by A83,A95,FUNCOP_1:7;
    hence contradiction by A82,A93,A67,A78,A68,A94,Def7;
  end;
  hence thesis by TARSKI:1;
end;

begin :: 9. Applications

definition
  let X be set, F be Dependency-set of X;
  attr F is (DC4) means
  :Def28:
  for A, B, C being Subset of X st [A, B] in F &
  [A, C] in F holds [A, B\/C] in F;
  attr F is (DC5) means
  :Def29:
  for A, B, C, D being Subset of X st [A, B] in
  F & [B\/C, D] in F holds [A\/C, D] in F;
  attr F is (DC6) means
  :Def30:
  for A, B, C being Subset of X st [A, B] in F holds [A\/C, B] in F;
end;

theorem :: APP0:
  for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3)
  (F4) iff F is (F2) (DC3) (F4);

theorem :: APP1:
  for X being set, F being 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,Def13;
      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 A7,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,Def15;
  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,Def15;
  then [A\/A9, B] in F by A7,A10,Th18;
  hence thesis by A9,A12,Def28;
end;

theorem :: APP2:
  for X being set, F being 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,Def11;
      then [A\/C, B\/C] in F by A4,A5,Def13;
      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,Def30;
    then [A\/A, C] in F by A9,A12,Def29;
    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,Th13;
    then A9 = A\/(A9\A) by XBOOLE_1:45;
    then
A16: [A9, B] in F by A10,A14,Def30;
    B9 c= B by A15,Th13;
    then
A17: B = B9\/(B\B9) by XBOOLE_1:45;
    [B9, B9] in F by A8,Def11;
    then [ B, B9] in F by A10,A17,Def30;
    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,Def11;
  then [A\/B9, B\/B9] in F by A9,A18,Def29;
  hence thesis by A9,A19,Def29;
end;

definition
  let X be set, F be Dependency-set of X;
  func charact_set F equals
  { A where A is Subset of X : ex a, b being Subset
  of X st [a, b] in F & a c= A & not b c= A };
  correctness;
end;

theorem Th55:
  for X, A being set, F being Dependency-set of X st A in
charact_set F holds A is Subset of X & ex a, b being 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 being Subset of X st A = Y & ex a, b being Subset of X st [a, b] in
  F & a c= Y & not b c= Y;
  hence thesis;
end;

theorem
  for X being set, A being Subset of X, F being Dependency-set of X st
  ex a, b being Subset of X st [a, b] in F & a c= A & not b c= A holds A in
  charact_set F;

theorem Th57: ::  WWA7:
  for X being finite non empty set, F being Dependency-set of X
holds (for A, B being Subset of X holds [A, B] in Dependency-closure F iff for
  a being 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 is Subset of A : for x, y being Subset of A st [x, y] in
  F & x c= b holds y c= b};
  now
    let c be set;
    hereby
      assume
A1:   c in B;
      then not c in charact_set F by XBOOLE_0:def 5;
      then
      for x, y being Subset of A st [x,y] in F & x c= c holds y c= c by A1;
      hence c in BB by A1;
    end;
    assume c in BB;
    then consider b being Subset of A such that
A2: c = b and
A3: for x, y being 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:1;
  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 is Subset of A : for c being 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 being Subset of A such that
A11:  [a9,b9] = [X,Y] and
A12:  for c being 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 being 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) by Def4;
  G = FF by A10,A8,XBOOLE_0:def 10;
  hence thesis by A21,A6,A7,Th35;
end;

theorem :: WWACorA: :: Bill: Is this the right translation
  for X being finite non empty set, F, G being 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 set;
    hereby
      assume
A2:   x in DCF;
      then consider a, b being 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 being 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:1;
end;

theorem Th59:
  for X being non empty finite set, F being 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 is Subset of X : for x, y being Subset of X st [x, y]
    in F & x c= c holds y c= c};
    let A be set;
    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 being Subset of X st [x, y] in F & x c= A & not y c= A
      by A2,Th55;
      hence A in charact_set dcF by A1,A3;
    end;
    assume
A4: A in charact_set dcF;
    then consider x, y being Subset of X such that
A5: [x, y] in dcF and
A6: x c= A and
A7: not y c= A by Th55;
A8: A is Subset of X by A4,Th55;
    assume not A in charact_set F;
    then for x, y being Subset of X st [x, y] in F & x c= A holds y c= A 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 being Subset of X such that
A10: [x, y] = [a,b] and
A11: for c being 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:1;
end;

definition
  let A be set, K be set, F be Dependency-set of A;
  pred K is_p_i_w_ncv_of F means
  : Def32:
  ( for a being Subset of A st K c= a
  & a <> A holds a in charact_set F) & for k being set st k c< K ex a being
  Subset of A st k c= a & a <> A & not a in charact_set F;
end;

theorem :: WWACorB:
  for X being finite non empty set, F being Dependency-set of X, K being
  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 is Subset of X : [K, P] in dcF };
  S c= bool X
  proof
    let x be set;
    assume x in S;
    then ex P being 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 is Subset of X : for x, y being 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 being set such that
A1: m in S and
A2: for B being 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 being Subset of X such that
A4: K = A and
A5: [A, X] in Maximal_wrt dcF;
A6: A ^|^ X, dcF by A5,Def17;
    [A, [#]X] in dcF by A5;
    then consider a, b being Subset of X such that
A7: [A,X] = [a,b] and
A8: for c being 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 being 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 is Subset of X : [k, P] in dcF };
      S c= bool X
      proof
        let x be set;
        assume x in S;
        then ex P being 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 being set such that
A15:  m in S and
A16:  for B being set st B in S holds m c= B implies B =m by FINSET_1:6;
      consider P being 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 being 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,10;
        end;
      end;
      k c= K by A14,XBOOLE_0:def 8;
      then [K,[#]X] <= [k,[#]X] by Th13;
      hence contradiction by A4,A6,A14,A21,Th27;
    end;
  end;
  consider P being 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,Def32;
      then K\/P in charact_set dcF by Th59;
      then consider x, y being 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,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,Th13;
    x9 c= K by A38,Th13;
    then x9 c< K by A37,A39,XBOOLE_0:def 8,def 10;
    then consider a being Subset of X such that
A40: x9 c= a and
A41: a <> X and
A42: not a in charact_set F by A29,Def32;
    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 by Def17;
  hence thesis;
end;