:: Introduction to Concept Lattices
::  by Christoph Schwarzweller
::
:: Received October 2, 1998
:: Copyright (c) 1998-2016 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 STRUCT_0, XBOOLE_0, RELAT_1, CAT_1, SUBSET_1, TARSKI, FUNCT_1,
      ZFMISC_1, MCART_1, YELLOW_1, LATTICE3, ORDERS_2, FILTER_1, WAYBEL_1,
      WAYBEL_0, XXREAL_0, PBOOLE, EQREL_1, CLASSES2, BINOP_1, LATTICES,
      QC_LANG1, REWRITE1, SETFAM_1, CONLAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, LATTICES,
      ORDERS_2, YELLOW_1, WAYBEL_1, LATTICE3, SETFAM_1, WAYBEL_0;
 constructors BINOP_1, DOMAIN_1, LATTICE3, WAYBEL_1, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES,
      LATTICE3, YELLOW_1, XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI;
 equalities TARSKI, BINOP_1;
 expansions TARSKI;
 theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, LATTICES, LATTICE3,
      YELLOW_1, ORDERS_2, FILTER_1, VECTSP_8, SETFAM_1, WAYBEL_0, RELSET_1,
      XBOOLE_0, XBOOLE_1, XTUPLE_0;
 schemes BINOP_1;

begin

registration
  cluster strict non empty non void for 2-sorted;
  existence
  proof
    2-sorted(#{{}},{{}}#) is non empty non void;
    hence thesis;
  end;
end;

definition
::$CD
  struct (2-sorted) ContextStr (# carrier, carrier' -> set, Information ->
    Relation of the carrier,the carrier' #);
end;

registration
  cluster strict non empty non void for ContextStr;
  existence
  proof
    ContextStr(#{{}},{{}},the Relation of {{}},{{}}#) is non empty non void;
    hence thesis;
  end;
end;

definition
  mode FormalContext is non empty non void ContextStr;
end;

definition
  let C be 2-sorted;
  mode Object of C is Element of C;
  mode Attribute of C is Element of the carrier' of C;
end;

registration
  let C be non empty non void 2-sorted;
  cluster the carrier' of C -> non empty;
  coherence;
  cluster the carrier of C -> non empty;
  coherence;
end;

registration
  let C be non empty non void 2-sorted;
  cluster non empty for Subset of the carrier of C;
  existence
  proof
    take the carrier of C;
    the carrier of C c= the carrier of C;
    hence thesis;
  end;
  cluster non empty for Subset of the carrier' of C;
  existence
  proof
    take the carrier' of C;
    the carrier' of C c= the carrier' of C;
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  let o be Object of C;
  let a be Attribute of C;

  pred o is-connected-with a means

  [o,a] in the Information of C;
end;

notation
  let C be FormalContext;
  let o be Object of C;
  let a be Attribute of C;
  antonym o is-not-connected-with a for o is-connected-with a;
end;

:: Derivation Operators

begin

definition
  let C be FormalContext;
  func ObjectDerivation(C) -> Function of bool the carrier of C,bool the
  carrier' of C means
  :Def2:
  for O being Subset of the carrier of C holds it.O =
  { a where a is Attribute of C : for o being Object of C st o in O holds o
  is-connected-with a };
  existence
  proof
    set f = the set of all
[O,{a where a is Attribute of C : for o being Object of C st o in
    O holds o is-connected-with a}] where O is Subset of the carrier of C ;
    for u being object st u in f holds ex v,w being object st u = [v,w]
    proof
      let u be object;
      assume u in f;
      then ex O being Subset of the carrier of C st u = [O,{a where a is
Attribute of C : for o being Object of C st o in O holds o is-connected-with a}
      ];
      hence thesis;
    end;
    then reconsider f as Relation by RELAT_1:def 1;
    for u,v1,v2 being object st [u,v1] in f & [u,v2] in f holds v1 = v2
    proof
      let u,v1,v2 be object;
      assume that
A1:   [u,v1] in f and
A2:   [u,v2] in f;
      consider O being Subset of the carrier of C such that
A3:   [u,v1] = [O,{a where a is Attribute of C : for o being Object of
      C st o in O holds o is-connected-with a}] by A1;
A4:   v1 = [u,v1]`2
       .= [O,{a where a is Attribute of C : for o being Object of C st o
      in O holds o is-connected-with a}]`2 by A3
        .= {a where a is Attribute of C : for o being Object of C st o in O
      holds o is-connected-with a};
      consider O9 being Subset of the carrier of C such that
A5:   [u,v2] = [O9,{a where a is Attribute of C : for o being Object
      of C st o in O9 holds o is-connected-with a}] by A2;
A6:   v2 = [u,v2]`2
       .= [O9,{a where a is Attribute of C : for o being Object of C st
      o in O9 holds o is-connected-with a}]`2 by A5
        .= {a where a is Attribute of C : for o being Object of C st o in O9
      holds o is-connected-with a}                 ;
      O = [O,{a where a is Attribute of C : for o being Object of C st o
      in O holds o is-connected-with a}]`1
        .= [u,v1]`1 by A3
        .= u
        .= [u,v2]`1
        .= [O9,{a where a is Attribute of C : for o being Object of C st o
      in O9 holds o is-connected-with a}]`1 by A5
        .= O9;
      hence thesis by A4,A6;
    end;
    then reconsider f as Function by FUNCT_1:def 1;
A7: for x being object holds x in dom f implies x in bool the carrier of C
    proof
      let x be object;
      assume x in dom f;
      then consider y being object such that
A8:   [x,y] in f by XTUPLE_0:def 12;
      consider O being Subset of the carrier of C such that
A9:   [x,y] = [O,{a where a is Attribute of C : for o being Object of
      C st o in O holds o is-connected-with a}] by A8;
      x = [x,y]`1
        .= [O,{a where a is Attribute of C : for o being Object of
      C st o in O holds o is-connected-with a}]`1 by A9
        .= O;
      hence thesis;
    end;
    for x being object holds x in bool the carrier of C implies x in dom f
    proof
      let x be object;
      assume x in bool the carrier of C;
      then reconsider x as Subset of the carrier of C;
      [x,{a where a is Attribute of C : for o being Object of C st o in x
      holds o is-connected-with a}] in f;
      hence thesis by XTUPLE_0:def 12;
    end;
    then
A10: dom f = bool the carrier of C by A7,TARSKI:2;
    rng f c= bool the carrier' of C
    proof
      let y be object;
      assume y in rng f;
      then consider x being object such that
A11:  [x,y] in f by XTUPLE_0:def 13;
      consider O being Subset of the carrier of C such that
A12:  [x,y] = [O,{a where a is Attribute of C : for o being Object of
      C st o in O holds o is-connected-with a}] by A11;
A13:  {a where a is Attribute of C : for o being Object of C st o in O
      holds o is-connected-with a} c= the carrier' of C
      proof
        let u be object;
        assume u in {a where a is Attribute of C : for o being Object of C
        st o in O holds o is-connected-with a};
        then ex u9 being Attribute of C st u9 = u & for o being Object of C st
        o in O holds o is-connected-with u9;
        hence thesis;
      end;
      y = [x,y]`2
       .= [O,{a where a is Attribute of C : for o being Object of
      C st o in O holds o is-connected-with a}]`2 by A12
        .= {a where a is Attribute of C : for o being Object of C st o in O
      holds o is-connected-with a};
      hence thesis by A13;
    end;
    then reconsider
    f as Function of bool the carrier of C,bool the carrier' of C
    by A10,FUNCT_2:def 1,RELSET_1:4;
    take f;
    for O being Subset of the carrier of C holds f.O = {a where a is
Attribute of C : for o being Object of C st o in O holds o is-connected-with a}
    proof
      let O be Subset of the carrier of C;
      consider y being object such that
A14:  [O,y] in f by A10,XTUPLE_0:def 12;
      consider O9 being Subset of the carrier of C such that
A15:  [O,y] = [O9,{a where a is Attribute of C : for o being Object
      of C st o in O9 holds o is-connected-with a}] by A14;
A16:  y = [O,y]`2
       .= [O9,{a where a is Attribute of C : for o being Object
      of C st o in O9 holds o is-connected-with a}]`2 by A15
        .= {a where a is Attribute of C : for o being Object of C st o in O9
      holds o is-connected-with a};
      O = [O,y]`1
        .= [O9,{a where a is Attribute of C : for o being Object
      of C st o in O9 holds o is-connected-with a}]`1 by A15
        .= O9;
      hence thesis by A10,A14,A16,FUNCT_1:def 2;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let F1,F2 be Function of bool the carrier of C,bool the carrier' of C;
    assume
A17: for O being Subset of the carrier of C holds F1.O = {a where a is
Attribute of C : for o being Object of C st o in O holds o is-connected-with a}
    ;
    assume
A18: for O being Subset of the carrier of C holds F2.O = {a where a is
Attribute of C : for o being Object of C st o in O holds o is-connected-with a}
    ;
A19: for O being object st O in bool the carrier of C holds F1.O = F2.O
    proof
      let O be object;
      assume O in bool the carrier of C;
      then reconsider O as Subset of the carrier of C;
      F1.O = {a where a is Attribute of C : for o being Object of C st o
      in O holds o is-connected-with a} by A17
        .= F2.O by A18;
      hence thesis;
    end;
    dom F1 = bool the carrier of C & dom F2 = bool the carrier of C by
FUNCT_2:def 1;
    hence thesis by A19,FUNCT_1:2;
  end;
end;

definition
  let C be FormalContext;
  func AttributeDerivation(C) -> Function of bool the carrier' of C,bool the
  carrier of C means
  :Def3:
  for A being Subset of the carrier' of C holds it.A =
  { o where o is Object of C : for a being Attribute of C st a in A holds o
  is-connected-with a };
  existence
  proof
    set f = the set of all
[A,{o where o is Object of C : for a being Attribute of C st a in
A holds o is-connected-with a}] where A is Subset of the carrier' of C ;
    for u being object st u in f holds ex v,w being object st u = [v,w]
    proof
      let u be object;
      assume u in f;
      then
      ex A being Subset of the carrier' of C st u = [A,{o where o is Object
      of C : for a being Attribute of C st a in A holds o is-connected-with a}]
      ;
      hence thesis;
    end;
    then reconsider f as Relation by RELAT_1:def 1;
    for u,v1,v2 being object st [u,v1] in f & [u,v2] in f holds v1 = v2
    proof
      let u,v1,v2 be object;
      assume that
A1:   [u,v1] in f and
A2:   [u,v2] in f;
      consider A being Subset of the carrier' of C such that
A3:   [u,v1] = [A,{o where o is Object of C : for a being Attribute of
      C st a in A holds o is-connected-with a}] by A1;
A4:   v1 =[u,v1]`2
       .= [A,{o where o is Object of C : for a being Attribute of C st a
      in A holds o is-connected-with a}]`2 by A3
        .= {o where o is Object of C : for a being Attribute of C st a in A
      holds o is-connected-with a};
      consider A9 being Subset of the carrier' of C such that
A5:   [u,v2] = [A9,{o where o is Object of C : for a being Attribute
      of C st a in A9 holds o is-connected-with a}] by A2;
A6:   v2 = [u,v2]`2
       .=[A9,{o where o is Object of C : for a being Attribute
      of C st a in A9 holds o is-connected-with a}]`2 by A5
       .= [A9,{o where o is Object of C : for a being Attribute of C st
      a in A9 holds o is-connected-with a}] `2
        .= {o where o is Object of C : for a being Attribute of C st a in A9
      holds o is-connected-with a};
      A = [A,{o where o is Object of C : for a being Attribute of C st a
      in A holds o is-connected-with a}]`1
        .= [u,v1]`1 by A3
        .= u
        .= [u,v2]`1
        .= [A9,{o where o is Object of C : for a being Attribute of C st a
      in A9 holds o is-connected-with a}]`1 by A5
        .= A9;
      hence thesis by A4,A6;
    end;
    then reconsider f as Function by FUNCT_1:def 1;
A7: for x being object holds x in dom f implies x in bool the carrier' of C
    proof
      let x be object;
      assume x in dom f;
      then consider y being object such that
A8:   [x,y] in f by XTUPLE_0:def 12;
      consider A being Subset of the carrier' of C such that
A9:   [x,y] = [A,{o where o is Object of C : for a being Attribute of
      C st a in A holds o is-connected-with a}] by A8;
      x = [x,y]`1
       .=[A,{o where o is Object of C : for a being Attribute of
      C st a in A holds o is-connected-with a}]`1 by A9
        .= A;
      hence thesis;
    end;
    for x being object holds x in bool the carrier' of C implies x in dom f
    proof
      let x be object;
      assume x in bool the carrier' of C;
      then reconsider x as Subset of the carrier' of C;
      [x,{o where o is Object of C : for a being Attribute of C st a in x
      holds o is-connected-with a}] in f;
      hence thesis by XTUPLE_0:def 12;
    end;
    then
A10: dom f = bool the carrier' of C by A7,TARSKI:2;
    rng f c= bool the carrier of C
    proof
      let y be object;
      assume y in rng f;
      then consider x being object such that
A11:  [x,y] in f by XTUPLE_0:def 13;
      consider A being Subset of the carrier' of C such that
A12:  [x,y] = [A,{o where o is Object of C : for a being Attribute of
      C st a in A holds o is-connected-with a}] by A11;
A13:  {o where o is Object of C : for a being Attribute of C st a in A
      holds o is-connected-with a} c= the carrier of C
      proof
        let u be object;
        assume u in {o where o is Object of C : for a being Attribute of C
        st a in A holds o is-connected-with a};
        then ex u9 being Object of C st u9 = u & for a being Attribute of C st
        a in A holds u9 is-connected-with a;
        hence thesis;
      end;
      y = [x,y]`2
        .=[A,{o where o is Object of C : for a being Attribute of
      C st a in A holds o is-connected-with a}]`2 by A12
        .= {o where o is Object of C : for a being Attribute of C st a in A
      holds o is-connected-with a};
      hence thesis by A13;
    end;
    then reconsider
    f as Function of bool the carrier' of C,bool the carrier of C
    by A10,FUNCT_2:def 1,RELSET_1:4;
    take f;
    for A being Subset of the carrier' of C holds f.A = {o where o is
Object of C : for a being Attribute of C st a in A holds o is-connected-with a}
    proof
      let A be Subset of the carrier' of C;
      consider y being object such that
A14:  [A,y] in f by A10,XTUPLE_0:def 12;
      consider A9 being Subset of the carrier' of C such that
A15:  [A,y] = [A9,{o where o is Object of C : for a being Attribute
      of C st a in A9 holds o is-connected-with a}] by A14;
A16:  y = [A,y]`2
        .=[A9,{o where o is Object of C : for a being Attribute
      of C st a in A9 holds o is-connected-with a}]`2 by A15
        .= {o where o is Object of C : for a being Attribute of C st a in A9
      holds o is-connected-with a};
      A = [A,y]`1
       .=[A9,{o where o is Object of C : for a being Attribute
      of C st a in A9 holds o is-connected-with a}]`1 by A15
        .= A9;
      hence thesis by A10,A14,A16,FUNCT_1:def 2;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let F1,F2 be Function of bool the carrier' of C,bool the carrier of C;
    assume
A17: for A being Subset of the carrier' of C holds F1.A = {o where o
is Object of C : for a being Attribute of C st a in A holds o is-connected-with
    a};
    assume
A18: for A being Subset of the carrier' of C holds F2.A = {o where o
is Object of C : for a being Attribute of C st a in A holds o is-connected-with
    a};
A19: for A being object st A in bool the carrier' of C holds F1.A = F2.A
    proof
      let A be object;
      assume A in bool the carrier' of C;
      then reconsider A as Subset of the carrier' of C;
      F1.A = {o where o is Object of C : for a being Attribute of C st a
      in A holds o is-connected-with a} by A17
        .= F2.A by A18;
      hence thesis;
    end;
    dom F1 = bool the carrier' of C & dom F2 = bool the carrier' of C by
FUNCT_2:def 1;
    hence thesis by A19,FUNCT_1:2;
  end;
end;

theorem
  for C being FormalContext for o being Object of C holds (
ObjectDerivation(C)).({o}) = {a where a is Attribute of C : o is-connected-with
  a}
proof
  let C be FormalContext;
  let o be Object of C;
  {o} c= the carrier of C
  proof
    let x be object;
    assume x in {o};
    then x = o by TARSKI:def 1;
    hence thesis;
  end;
  then reconsider t = {o} as Subset of the carrier of C;
A1: for x being object holds x in {a where a is Attribute of C : for o9 being
Object of C st o9 in t holds o9 is-connected-with a} implies x in {a where a is
  Attribute of C : o is-connected-with a}
  proof
    set o9 = the Element of t;
    let x be object;
    reconsider o9 as Object of C by TARSKI:def 1;
A2: o9 = o by TARSKI:def 1;
    assume x in {a where a is Attribute of C : for o9 being Object of C st o9
    in t holds o9 is-connected-with a};
    then
A3: ex x9 being Attribute of C st x9 = x & for o9 being Object of C st o9
    in t holds o9 is-connected-with x9;
    then reconsider x as Attribute of C;
    o9 is-connected-with x by A3;
    hence thesis by A2;
  end;
A4: for x being object holds x in {a where a is Attribute of C : o
  is-connected-with a} implies x in {a where a is Attribute of C : for o9 being
  Object of C st o9 in t holds o9 is-connected-with a}
  proof
    let x be object;
    assume x in {a where a is Attribute of C : o is-connected-with a};
    then
A5: ex x9 being Attribute of C st x9 = x & o is-connected-with x9;
    then reconsider x as Attribute of C;
    for o9 being Object of C st o9 in t holds o9 is-connected-with x by A5,
TARSKI:def 1;
    hence thesis;
  end;
  (ObjectDerivation(C)).t = {a where a is Attribute of C : for o9 being
  Object of C st o9 in t holds o9 is-connected-with a} by Def2;
  hence thesis by A1,A4,TARSKI:2;
end;

theorem
  for C being FormalContext for a being Attribute of C holds (
AttributeDerivation(C)).({a}) = {o where o is Object of C : o is-connected-with
  a}
proof
  let C be FormalContext;
  let a be Attribute of C;
  {a} c= the carrier' of C
  proof
    let x be object;
    assume x in {a};
    then x = a by TARSKI:def 1;
    hence thesis;
  end;
  then reconsider t = {a} as Subset of the carrier' of C;
A1: for x being object holds x in {o where o is Object of C : for a9 being
Attribute of C st a9 in t holds o is-connected-with a9} implies x in {o where o
  is Object of C : o is-connected-with a}
  proof
    set a9 = the Element of t;
    let x be object;
    reconsider a9 as Attribute of C by TARSKI:def 1;
A2: a9 = a by TARSKI:def 1;
    assume x in {o where o is Object of C : for a9 being Attribute of C st a9
    in t holds o is-connected-with a9};
    then
A3: ex x9 being Object of C st x9 = x & for a9 being Attribute of C st a9
    in t holds x9 is-connected-with a9;
    then reconsider x as Object of C;
    x is-connected-with a9 by A3;
    hence thesis by A2;
  end;
A4: for x being object holds x in {o where o is Object of C : o
  is-connected-with a} implies x in {o where o is Object of C : for a9 being
  Attribute of C st a9 in t holds o is-connected-with a9}
  proof
    let x be object;
    assume x in {o where o is Object of C : o is-connected-with a};
    then
A5: ex x9 being Object of C st x9 = x & x9 is-connected-with a;
    then reconsider x as Object of C;
    for a9 being Attribute of C st a9 in t holds x is-connected-with a9
    by A5,TARSKI:def 1;
    hence thesis;
  end;
  (AttributeDerivation(C)).t = {o where o is Object of C : for a9 being
  Attribute of C st a9 in t holds o is-connected-with a9} by Def3;
  hence thesis by A1,A4,TARSKI:2;
end;

theorem Th3:
  for C being FormalContext for O1,O2 being Subset of the carrier
of C holds O1 c= O2 implies (ObjectDerivation(C)).O2 c= (ObjectDerivation(C)).
  O1
proof
  let C be FormalContext;
  let O1,O2 be Subset of the carrier of C;
  assume
A1: O1 c= O2;
  let x be object;
  assume x in (ObjectDerivation(C)).O2;
  then x in {a where a is Attribute of C : for o being Object of C st o in O2
  holds o is-connected-with a} by Def2;
  then consider x9 being Attribute of C such that
A2: x9 = x and
A3: for o being Object of C st o in O2 holds o is-connected-with x9;
  for o being Object of C st o in O1 holds o is-connected-with x9 by A1,A3;
  then x in {a where a is Attribute of C : for o being Object of C st o in O1
  holds o is-connected-with a} by A2;
  hence thesis by Def2;
end;

theorem Th4:
  for C being FormalContext for A1,A2 being Subset of the carrier'
of C holds A1 c= A2 implies (AttributeDerivation(C)).A2 c= (AttributeDerivation
  (C)).A1
proof
  let C be FormalContext;
  let A1,A2 be Subset of the carrier' of C;
  assume
A1: A1 c= A2;
  let x be object;
  assume x in (AttributeDerivation(C)).A2;
  then x in {o where o is Object of C : for a being Attribute of C st a in A2
  holds o is-connected-with a} by Def3;
  then consider x9 being Object of C such that
A2: x9 = x and
A3: for a being Attribute of C st a in A2 holds x9 is-connected-with a;
  for a being Attribute of C st a in A1 holds x9 is-connected-with a by A1,A3;
  then x in {o where o is Object of C : for a being Attribute of C st a in A1
  holds o is-connected-with a} by A2;
  hence thesis by Def3;
end;

theorem Th5:
  for C being FormalContext for O being Subset of the carrier of C
  holds O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O)
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
  set A = {a where a is Attribute of C : for o being Object of C st o in O
  holds o is-connected-with a};
  for x being object holds x in A implies x in the carrier' of C
  proof
    let x be object;
    assume x in A;
    then
    ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    O holds o is-connected-with x9;
    hence thesis;
  end;
  then reconsider A as Subset of the carrier' of C by TARSKI:def 3;
  let x be object;
  assume
A1: x in O;
  then reconsider x as Object of C;
A2: for a being Attribute of C st a in A holds x is-connected-with a
  proof
    let a be Attribute of C;
    assume a in A;
    then
    ex a9 being Attribute of C st a9 = a & for o being Object of C st o in
    O holds o is-connected-with a9;
    hence thesis by A1;
  end;
  (AttributeDerivation(C)).A = {o where o is Object of C : for a being
  Attribute of C st a in A holds o is-connected-with a} by Def3;
  then x in (AttributeDerivation(C)).A by A2;
  hence thesis by Def2;
end;

theorem Th6:
  for C being FormalContext for A being Subset of the carrier' of C
  holds A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A)
proof
  let C be FormalContext;
  let A be Subset of the carrier' of C;
  set O = {o where o is Object of C : for a being Attribute of C st a in A
  holds o is-connected-with a};
  for x being object holds x in O implies x in the carrier of C
  proof
    let x be object;
    assume x in O;
    then
    ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A holds x9 is-connected-with a;
    hence thesis;
  end;
  then reconsider O as Subset of the carrier of C by TARSKI:def 3;
  let x be object;
  assume
A1: x in A;
  then reconsider x as Attribute of C;
A2: for o being Object of C st o in O holds o is-connected-with x
  proof
    let o be Object of C;
    assume o in O;
    then
    ex o9 being Object of C st o9 = o & for a being Attribute of C st a in
    A holds o9 is-connected-with a;
    hence thesis by A1;
  end;
  (ObjectDerivation(C)).O = {a where a is Attribute of C : for o being
  Object of C st o in O holds o is-connected-with a} by Def2;
  then x in (ObjectDerivation(C)).O by A2;
  hence thesis by Def3;
end;

theorem Th7:
  for C being FormalContext for O being Subset of the carrier of C
holds (ObjectDerivation(C)).O = (ObjectDerivation(C)).((AttributeDerivation(C))
  .((ObjectDerivation(C)).O))
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
  set A = {a where a is Attribute of C : for o being Object of C st o in O
  holds o is-connected-with a};
  set O9 = {o where o is Object of C : for a being Attribute of C st a in A
  holds o is-connected-with a};
  set A9 = {a where a is Attribute of C : for o being Object of C st o in O9
  holds o is-connected-with a};
A1: for x being object holds x in A9 implies x in A
  proof
    let x be object;
    assume x in A9;
    then
A2: ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    O9 holds o is-connected-with x9;
    then reconsider x as Attribute of C;
    for o being Object of C st o in O holds o is-connected-with x
    proof
      let o be Object of C;
      assume
A3:   o in O;
      now
        per cases;
        case
          o in O9;
          hence thesis by A2;
        end;
        case
          not o in O9;
          then consider a being Attribute of C such that
A4:       a in A and
A5:       not o is-connected-with a;
          ex a9 being Attribute of C st a9 = a & for o being Object of C
          st o in O holds o is-connected-with a9 by A4;
          hence thesis by A3,A5;
        end;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  for x being object holds x in A implies x in A9
  proof
    let x be object;
    assume
A6: x in A;
    then
    ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    O holds o is-connected-with x9;
    then reconsider x as Attribute of C;
    for o being Object of C st o in O9 holds o is-connected-with x
    proof
      let o be Object of C;
      assume o in O9;
      then ex o9 being Object of C st o9 = o & for a being Attribute of C st a
      in A holds o9 is-connected-with a;
      hence thesis by A6;
    end;
    hence thesis;
  end;
  then
A7: A = A9 by A1,TARSKI:2;
  A c= the carrier' of C
  proof
    let x be object;
    assume x in A;
    then
    ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    O holds o is-connected-with x9;
    hence thesis;
  end;
  then reconsider A as Subset of the carrier' of C;
  O9 c= the carrier of C
  proof
    let x be object;
    assume x in O9;
    then
    ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A holds x9 is-connected-with a;
    hence thesis;
  end;
  then reconsider O9 as Subset of the carrier of C;
  A = (ObjectDerivation(C)).O & O9 = (AttributeDerivation(C)).A by Def2,Def3;
  hence thesis by A7,Def2;
end;

theorem Th8:
  for C being FormalContext for A being Subset of the carrier' of C
holds (AttributeDerivation(C)).A = (AttributeDerivation(C)).((ObjectDerivation(
  C)).((AttributeDerivation(C)).A))
proof
  let C be FormalContext;
  let A be Subset of the carrier' of C;
  set O = {o where o is Object of C : for a being Attribute of C st a in A
  holds o is-connected-with a};
  set A9 = {a where a is Attribute of C : for o being Object of C st o in O
  holds o is-connected-with a};
  set O9 = {o where o is Object of C : for a being Attribute of C st a in A9
  holds o is-connected-with a};
A1: for x being object holds x in O9 implies x in O
  proof
    let x be object;
    assume x in O9;
    then
A2: ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A9 holds x9 is-connected-with a;
    then reconsider x as Object of C;
    for a being Attribute of C st a in A holds x is-connected-with a
    proof
      let a be Attribute of C;
      assume
A3:   a in A;
      now
        per cases;
        case
          a in A9;
          hence thesis by A2;
        end;
        case
          not a in A9;
          then consider o being Object of C such that
A4:       o in O and
A5:       not o is-connected-with a;
          ex o9 being Object of C st o9 = o & for a being Attribute of C
          st a in A holds o9 is-connected-with a by A4;
          hence thesis by A3,A5;
        end;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  for x being object holds x in O implies x in O9
  proof
    let x be object;
    assume
A6: x in O;
    then
    ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A holds x9 is-connected-with a;
    then reconsider x as Object of C;
    for a being Attribute of C st a in A9 holds x is-connected-with a
    proof
      let a be Attribute of C;
      assume a in A9;
      then ex a9 being Attribute of C st a9 = a & for o being Object of C st o
      in O holds o is-connected-with a9;
      hence thesis by A6;
    end;
    hence thesis;
  end;
  then
A7: O = O9 by A1,TARSKI:2;
  O c= the carrier of C
  proof
    let x be object;
    assume x in O;
    then
    ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A holds x9 is-connected-with a;
    hence thesis;
  end;
  then reconsider O as Subset of the carrier of C;
  A9 c= the carrier' of C
  proof
    let x be object;
    assume x in A9;
    then
    ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    O holds o is-connected-with x9;
    hence thesis;
  end;
  then reconsider A9 as Subset of the carrier' of C;
  O = (AttributeDerivation(C)).A & A9 = (ObjectDerivation(C)).O by Def2,Def3;
  hence thesis by A7,Def3;
end;

theorem Th9:
  for C being FormalContext for O being Subset of the carrier of C
  for A being Subset of the carrier' of C holds O c= (AttributeDerivation(C)).A
  iff [:O,A:] c= the Information of C
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
  let A be Subset of the carrier' of C;
A1: [:O,A:] c= the Information of C implies O c= (AttributeDerivation(C)).A
  proof
    assume
A2: [:O,A:] c= the Information of C;
    let x be object;
    assume
A3: x in O;
    then reconsider x as Object of C;
    for a being Attribute of C st a in A holds x is-connected-with a
    proof
      let a be Attribute of C;
      consider z being set such that
A4:   z = [x,a];
      assume a in A;
      then z in [:O,A:] by A3,A4,ZFMISC_1:def 2;
      hence thesis by A2,A4;
    end;
    then
    x in {o where o is Object of C : for a being Attribute of C st a in A
    holds o is-connected-with a};
    hence thesis by Def3;
  end;
  O c= (AttributeDerivation(C)).A implies [:O,A:] c= the Information of C
  proof
    assume O c= (AttributeDerivation(C)).A;
    then
A5: O c= {o where o is Object of C : for a being Attribute of C st a in A
    holds o is-connected-with a} by Def3;
    let z be object;
    assume z in [:O,A:];
    then consider x,y being object such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def 2;
    reconsider y as Attribute of C by A7;
    reconsider x as Object of C by A6;
    x in {o where o is Object of C : for a being Attribute of C st a in A
    holds o is-connected-with a} by A5,A6;
    then
    ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A holds x9 is-connected-with a;
    then x is-connected-with y by A7;
    hence thesis by A8;
  end;
  hence thesis by A1;
end;

theorem Th10:
  for C being FormalContext for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds A c= (ObjectDerivation(C)).O iff
  [:O,A:] c= the Information of C
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
  let A be Subset of the carrier' of C;
A1: [:O,A:] c= the Information of C implies A c= (ObjectDerivation(C)).O
  proof
    assume
A2: [:O,A:] c= the Information of C;
    let x be object;
    assume
A3: x in A;
    then reconsider x as Attribute of C;
    for o being Object of C st o in O holds o is-connected-with x
    proof
      let o be Object of C;
      consider z being set such that
A4:   z = [o,x];
      assume o in O;
      then z in [:O,A:] by A3,A4,ZFMISC_1:def 2;
      hence thesis by A2,A4;
    end;
    then
    x in {a where a is Attribute of C : for o being Object of C st o in O
    holds o is-connected-with a};
    hence thesis by Def2;
  end;
  A c= (ObjectDerivation(C)).O implies [:O,A:] c= the Information of C
  proof
    assume A c= (ObjectDerivation(C)).O;
    then
A5: A c= {a where a is Attribute of C : for o being Object of C st o in O
    holds o is-connected-with a} by Def2;
    let z be object;
    assume z in [:O,A:];
    then consider x,y being object such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def 2;
    reconsider y as Attribute of C by A7;
    reconsider x as Object of C by A6;
    y in {a where a is Attribute of C : for o being Object of C st o in O
    holds o is-connected-with a} by A5,A7;
    then
    ex y9 being Attribute of C st y9 = y & for o being Object of C st o in
    O holds o is-connected-with y9;
    then x is-connected-with y by A6;
    hence thesis by A8;
  end;
  hence thesis by A1;
end;

theorem
  for C being FormalContext for O being Subset of the carrier of C for A
  being Subset of the carrier' of C holds O c= (AttributeDerivation(C)).A iff A
  c= (ObjectDerivation(C)).O
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
  let A be Subset of the carrier' of C;
  O c= (AttributeDerivation(C)).A iff [:O,A:] c= the Information of C by Th9;
  hence thesis by Th10;
end;

definition
  let C be FormalContext;
  func phi(C) -> Function of BoolePoset the carrier of C, BoolePoset the
  carrier' of C equals
  ObjectDerivation(C);
  coherence
  proof
A1: rng(ObjectDerivation(C)) c= the carrier of BoolePoset the carrier' of C
    proof
      let x be object;
      assume x in rng(ObjectDerivation(C));
      then x in bool the carrier' of C;
      then
A2:   x in the carrier of BooleLatt the carrier' of C by LATTICE3:def 1;
      LattPOSet BooleLatt the carrier' of C = RelStr (#the carrier of
BooleLatt the carrier' of C, LattRel BooleLatt the carrier' of C#) by
LATTICE3:def 2;
      hence thesis by A2,YELLOW_1:def 2;
    end;
A3: LattPOSet BooleLatt the carrier of C = RelStr (#the carrier of
BooleLatt the carrier of C, LattRel BooleLatt the carrier of C#) by
LATTICE3:def 2;
A4: for x being object holds x in the carrier of BoolePoset the carrier of C
    implies x in dom(ObjectDerivation(C))
    proof
      let x be object;
      assume x in the carrier of BoolePoset the carrier of C;
      then x in the carrier of LattPOSet BooleLatt the carrier of C by
YELLOW_1:def 2;
      then x in bool the carrier of C by A3,LATTICE3:def 1;
      hence thesis by FUNCT_2:def 1;
    end;
    for x being object holds x in dom(ObjectDerivation(C)) implies x in the
    carrier of BoolePoset the carrier of C
    proof
      let x be object;
      assume x in dom(ObjectDerivation(C));
      then x in bool the carrier of C;
      then x in the carrier of BooleLatt the carrier of C by LATTICE3:def 1;
      hence thesis by A3,YELLOW_1:def 2;
    end;
    then
    dom(ObjectDerivation(C)) = the carrier of BoolePoset the carrier of C
    by A4,TARSKI:2;
    then reconsider g = ObjectDerivation(C) as Function of the carrier of
    BoolePoset the carrier of C, the carrier of BoolePoset the carrier' of C
by A1,FUNCT_2:def 1,RELSET_1:4;
    g is Function of BoolePoset the carrier of C, BoolePoset the carrier' of C;
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  func psi(C) -> Function of BoolePoset the carrier' of C, BoolePoset the
  carrier of C equals
  AttributeDerivation(C);
  coherence
  proof
A1: rng(AttributeDerivation(C)) c= the carrier of BoolePoset(the carrier of C)
    proof
      let x be object;
      assume x in rng(AttributeDerivation(C));
      then x in bool the carrier of C;
      then
A2:   x in the carrier of (BooleLatt the carrier of C) by LATTICE3:def 1;
      LattPOSet BooleLatt the carrier of C = RelStr (#the carrier of
BooleLatt the carrier of C, LattRel BooleLatt the carrier of C#) by
LATTICE3:def 2;
      hence thesis by A2,YELLOW_1:def 2;
    end;
A3: LattPOSet BooleLatt the carrier' of C = RelStr (#the carrier of
BooleLatt the carrier' of C, LattRel BooleLatt the carrier' of C#) by
LATTICE3:def 2;
A4: for x being object holds x in the carrier of BoolePoset(the carrier' of C
    ) implies x in dom(AttributeDerivation(C))
    proof
      let x be object;
      assume x in the carrier of BoolePoset the carrier' of C;
      then x in the carrier of LattPOSet BooleLatt the carrier' of C by
YELLOW_1:def 2;
      then x in bool the carrier' of C by A3,LATTICE3:def 1;
      hence thesis by FUNCT_2:def 1;
    end;
    for x being object holds x in dom(AttributeDerivation(C)) implies x in
    the carrier of BoolePoset the carrier' of C
    proof
      let x be object;
      assume x in dom(AttributeDerivation(C));
      then x in bool the carrier' of C;
      then x in the carrier of BooleLatt the carrier' of C by LATTICE3:def 1;
      hence thesis by A3,YELLOW_1:def 2;
    end;
    then dom(AttributeDerivation(C)) = the carrier of BoolePoset the carrier'
    of C by A4,TARSKI:2;
    hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
  end;
end;

definition
  let P,R be non empty RelStr;
  let Con be Connection of P,R;
  attr Con is co-Galois means

  ex f being Function of P,R, g being
  Function of R,P st (Con = [f,g] & f is antitone & g is antitone & for p1,p2
being Element of P, r1,r2 being Element of R holds p1 <= g.(f.p1) & r1 <= f.(g.
  r1));
end;

theorem Th12:
  for P,R being non empty Poset for Con being Connection of P,R
  for f being Function of P,R, g being Function of R,P st Con = [f,g] holds Con
is co-Galois iff for p being Element of P, r being Element of R holds p <= g.r
  iff r <= f.p
proof
  let P,R be non empty Poset;
  let Con be Connection of P,R;
  let f be Function of P,R, g be Function of R,P;
  assume
A1: Con = [f,g];
A2: now
    assume
A3: for p being Element of P, r being Element of R holds p <= g.r iff r <= f.p;
    for p1,p2 being Element of P st p1 <= p2 for r1,r2 being Element of R
    st r1 = f.p1 & r2 = f.p2 holds r1 >= r2
    proof
      let p1,p2 be Element of P;
      assume
A4:   p1 <= p2;
      let r1,r2 be Element of R;
      assume
A5:   r1 = f.p1 & r2 = f.p2;
      p2 <= g.(f.p2) by A3;
      then p1 <= g.(f.p2) by A4,ORDERS_2:3;
      hence thesis by A3,A5;
    end;
    then
A6: f is antitone by WAYBEL_0:def 5;
    for r1,r2 being Element of R st r1 <= r2 for p1,p2 being Element of P
    st p1 = g.r1 & p2 = g.r2 holds p1 >= p2
    proof
      let r1,r2 be Element of R;
      assume
A7:   r1 <= r2;
      let p1,p2 be Element of P;
      assume
A8:   p1 = g.r1 & p2 = g.r2;
      r2 <= f.(g.r2) by A3;
      then r1 <= f.(g.r2) by A7,ORDERS_2:3;
      hence thesis by A3,A8;
    end;
    then
A9: g is antitone by WAYBEL_0:def 5;
    for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <= g.
    (f.p1) & r1 <= f.(g.r1) by A3;
    hence Con is co-Galois by A1,A6,A9;
  end;
  now
    assume Con is co-Galois;
    then consider f9 being Function of P,R, g9 being Function of R,P such that
A10: Con = [f9,g9] and
A11: f9 is antitone and
A12: g9 is antitone and
A13: for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <=
    g9.(f9.p1) & r1 <= f9.(g9.r1);
A14: g = [f,g]`2
      .= Con`2 by A1
      .= [f9,g9]`2 by A10
      .= g9;
A15: f = [f,g]`1
      .= Con`1 by A1
      .= [f9,g9]`1 by A10
      .= f9;
A16: for p being Element of P, r being Element of R holds r <= f.p implies
    p <= g.r
    proof
      let p be Element of P, r be Element of R;
      assume r <= f.p;
      then
A17:  g.r >= g.(f.p) by A12,A14,WAYBEL_0:def 5;
      p <= g.(f.p) by A13,A15,A14;
      hence thesis by A17,ORDERS_2:3;
    end;
    for p being Element of P, r being Element of R holds p <= g.r implies
    r <= f.p
    proof
      let p be Element of P, r be Element of R;
      assume p <= g.r;
      then
A18:  f.p >= f.(g.r) by A11,A15,WAYBEL_0:def 5;
      r <= f.(g.r) by A13,A15,A14;
      hence thesis by A18,ORDERS_2:3;
    end;
    hence for p being Element of P, r being Element of R holds p <= g.r iff r
    <= f.p by A16;
  end;
  hence thesis by A2;
end;

theorem
  for P,R being non empty Poset for Con being Connection of P,R st Con
is co-Galois for f being Function of P,R, g being Function of R,P st Con = [f,g
  ] holds f = f * (g * f) & g = g * (f * g)
proof
  let P,R be non empty Poset;
  let Con be Connection of P,R;
  assume Con is co-Galois;
  then consider f9 being Function of P,R, g9 being Function of R,P such that
A1: Con = [f9,g9] and
A2: f9 is antitone and
A3: g9 is antitone and
A4: for p1,p2 being Element of P, r1,r2 being Element of R holds p1 <=
  g9.(f9.p1) & r1 <= f9.(g9.r1);
  let f be Function of P,R, g be Function of R,P;
  assume
A5: Con = [f,g];
A6: f = [f,g]`1
    .= Con`1 by A5
    .= [f9,g9]`1 by A1
    .= f9;
A7: g = [f,g]`2
     .= Con`2 by A5
    .= [f9,g9]`2 by A1
    .= g9;
A8: dom g = the carrier of R by FUNCT_2:def 1;
A9: dom f = the carrier of P by FUNCT_2:def 1;
A10: for x being object st x in the carrier of P holds f.x =(f*(g*f)).x
  proof
    let x be object;
    assume x in the carrier of P;
    then reconsider x as Element of P;
    x <= g.(f.x) by A4,A6,A7;
    then
A11: f.x >= f.(g.(f.x)) by A2,A6,WAYBEL_0:def 5;
    f.x <= f.(g.(f.x)) by A4,A6,A7;
    then f.x = f.(g.(f.x)) by A11,ORDERS_2:2;
    then
A12: f.x = f.((g*f).x) by A9,FUNCT_1:13;
    f.x is Element of R;
    then x in dom (g*f) by A9,A8,FUNCT_1:11;
    hence thesis by A12,FUNCT_1:13;
  end;
A13: for x being object st x in the carrier of R holds g.x =(g*(f*g)).x
  proof
    let x be object;
    assume x in the carrier of R;
    then reconsider x as Element of R;
    x <= f.(g.x) by A4,A6,A7;
    then
A14: g.x >= g.(f.(g.x)) by A3,A7,WAYBEL_0:def 5;
    g.x <= g.(f.(g.x)) by A4,A6,A7;
    then g.x = g.(f.(g.x)) by A14,ORDERS_2:2;
    then
A15: g.x = g.((f*g).x) by A8,FUNCT_1:13;
    g.x is Element of P;
    then x in dom (f*g) by A9,A8,FUNCT_1:11;
    hence thesis by A15,FUNCT_1:13;
  end;
  dom (f*(g*f)) = the carrier of P & dom (g*(f*g)) = the carrier of R by
FUNCT_2:def 1;
  hence thesis by A9,A8,A10,A13,FUNCT_1:2;
end;

theorem
  for C being FormalContext holds [phi(C),psi(C)] is co-Galois
proof
  let C be FormalContext;
A1: LattPOSet BooleLatt the carrier' of C = RelStr (#the carrier of
BooleLatt the carrier' of C, LattRel BooleLatt the carrier' of C#) by
LATTICE3:def 2;
A2: LattPOSet BooleLatt the carrier of C = RelStr (#the carrier of BooleLatt
    the carrier of C, LattRel BooleLatt the carrier of C#) by LATTICE3:def 2;
A3: for x being Element of BoolePoset the carrier of C, y being Element of
  BoolePoset the carrier' of C st y <= (phi(C)).x holds x <= (psi(C)).y
  proof
    let x be Element of BoolePoset the carrier of C, y be Element of
    BoolePoset the carrier' of C;
    assume y <= (phi(C)).x;
    then [y,(phi(C)).x] in the InternalRel of (BoolePoset the carrier' of C)
    by ORDERS_2:def 5;
    then
A4: [y,(phi(C)).x] in LattRel (BooleLatt the carrier' of C) by A1,
YELLOW_1:def 2;
    reconsider x9 = (phi(C)).x as Element of (BooleLatt the carrier' of C) by
A1,YELLOW_1:def 2;
    reconsider x as Element of BooleLatt the carrier of C by A2,YELLOW_1:def 2;
    reconsider x as Subset of the carrier of C by LATTICE3:def 1;
    reconsider y as Element of (BooleLatt the carrier' of C) by A1,
YELLOW_1:def 2;
    y [= x9 by A4,FILTER_1:31;
    then
A5: y "\/" x9 = x9 by LATTICES:def 3;
    reconsider x9 as Subset of the carrier' of C by LATTICE3:def 1;
    reconsider y as Subset of the carrier' of C by LATTICE3:def 1;
    for z being object holds z in y implies z in x9 by A5,XBOOLE_0:def 3;
    then y c= x9;
    then
A6: (AttributeDerivation(C)).x9 c= (AttributeDerivation(C)).y by Th4;
    reconsider y as Element of BoolePoset the carrier' of C;
    reconsider y9 = (psi(C)).y as Element of (BooleLatt the carrier of C) by A2
,YELLOW_1:def 2;
    reconsider y9 as Subset of the carrier of C by LATTICE3:def 1;
    reconsider y9 as Element of (BooleLatt the carrier of C);
A7: x c= (AttributeDerivation(C)).((ObjectDerivation(C)).x) by Th5;
    reconsider x as Subset of the carrier of C;
    reconsider x as Element of (BooleLatt the carrier of C);
    x "\/" y9 = y9 by A6,A7,XBOOLE_1:1,12;
    then x [= y9 by LATTICES:def 3;
    then [x,(psi(C)).y] in LattRel (BooleLatt the carrier of C) by FILTER_1:31;
    then
    [x,(psi(C)).y] in the InternalRel of (BoolePoset the carrier of C) by A2,
YELLOW_1:def 2;
    hence thesis by ORDERS_2:def 5;
  end;
  for x being Element of BoolePoset the carrier of C, y being Element of
  BoolePoset the carrier' of C st x <= (psi(C)).y holds y <= (phi(C)).x
  proof
    let x be Element of BoolePoset the carrier of C, y be Element of
    BoolePoset the carrier' of C;
    assume x <= (psi(C)).y;
    then
    [x,(psi(C)).y] in the InternalRel of (BoolePoset the carrier of C) by
ORDERS_2:def 5;
    then
A8: [x,(psi(C)).y] in LattRel (BooleLatt the carrier of C) by A2,YELLOW_1:def 2
;
    reconsider y9 = (psi(C)).y as Element of (BooleLatt the carrier of C) by A2
,YELLOW_1:def 2;
    reconsider y as Element of (BooleLatt the carrier' of C) by A1,
YELLOW_1:def 2;
    reconsider y as Subset of the carrier' of C by LATTICE3:def 1;
    reconsider x as Element of (BooleLatt the carrier of C) by A2,
YELLOW_1:def 2;
    x [= y9 by A8,FILTER_1:31;
    then
A9: x "\/" y9 = y9 by LATTICES:def 3;
    reconsider y9 as Subset of the carrier of C by LATTICE3:def 1;
    reconsider x as Subset of the carrier of C by LATTICE3:def 1;
    for z being object holds z in x implies z in y9 by A9,XBOOLE_0:def 3;
    then
A10: x c= y9;
    reconsider x,y9 as Subset of the carrier of C;
A11: (ObjectDerivation(C)).y9 c= (ObjectDerivation(C)).x by A10,Th3;
    reconsider x as Element of BoolePoset the carrier of C;
    reconsider x9 = (phi(C)).x as Element of (BooleLatt the carrier' of C) by
A1,YELLOW_1:def 2;
    reconsider x9 as Subset of the carrier' of C by LATTICE3:def 1;
    reconsider x9 as Element of (BooleLatt the carrier' of C);
A12: y c= (ObjectDerivation(C)).((AttributeDerivation(C)).y) by Th6;
    reconsider y as Element of (BooleLatt the carrier' of C);
    y "\/" x9 = x9 by A11,A12,XBOOLE_1:1,12;
    then y [= x9 by LATTICES:def 3;
    then [y,(phi(C)).x] in LattRel (BooleLatt the carrier' of C) by FILTER_1:31
;
    then [y,(phi(C)).x] in the InternalRel of (BoolePoset the carrier' of C)
    by A1,YELLOW_1:def 2;
    hence thesis by ORDERS_2:def 5;
  end;
  hence thesis by A3,Th12;
end;

theorem Th15:
  for C being FormalContext for O1,O2 being Subset of the carrier
of C holds (ObjectDerivation(C)).(O1 \/ O2) = ((ObjectDerivation(C)).O1) /\ ((
  ObjectDerivation(C)).O2)
proof
  let C be FormalContext;
  let O1,O2 be Subset of the carrier of C;
  reconsider O9 = O1 \/ O2 as Subset of the carrier of C;
A1: for x being object holds x in (ObjectDerivation(C)).O1 /\ (
  ObjectDerivation( C ) ) . O2 implies x in (ObjectDerivation(C)).O9
  proof
    let x be object;
    assume
A2: x in (ObjectDerivation(C)).O1 /\ (ObjectDerivation(C)).O2;
    then x in (ObjectDerivation(C)).O1 by XBOOLE_0:def 4;
    then x in {a where a is Attribute of C : for o being Object of C st o in
    O1 holds o is-connected-with a} by Def2;
    then
A3: ex x1 being Attribute of C st x1 = x & for o being Object of C st o in
    O1 holds o is-connected-with x1;
    x in (ObjectDerivation(C)).O2 by A2,XBOOLE_0:def 4;
    then x in {a where a is Attribute of C : for o being Object of C st o in
    O2 holds o is-connected-with a } by Def2;
    then
A4: ex x2 being Attribute of C st x2 = x & for o being Object of C st o in
    O2 holds o is-connected-with x2;
    then reconsider x as Attribute of C;
    for o being Object of C st o in O1 \/ O2 holds o is-connected-with x
    proof
      let o be Object of C;
      assume
A5:   o in (O1 \/ O2);
      now
        per cases by A5,XBOOLE_0:def 3;
        case
          o in O1;
          hence thesis by A3;
        end;
        case
          o in O2;
          hence thesis by A4;
        end;
      end;
      hence thesis;
    end;
    then x in {a where a is Attribute of C : for o being Object of C st o in
    O9 holds o is-connected-with a};
    hence thesis by Def2;
  end;
  for x being object holds x in (ObjectDerivation(C)).(O1 \/ O2) implies x in
  (ObjectDerivation(C)).O1 /\ (ObjectDerivation(C)).O2
  proof
    let x be object;
    assume x in (ObjectDerivation(C)).(O1 \/ O2);
    then
    x in {a where a is Attribute of C : for o being Object of C st o in O9
    holds o is-connected-with a} by Def2;
    then
A6: ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    O9 holds o is-connected-with x9;
    then reconsider x as Attribute of C;
    for o being Object of C st o in O2 holds o is-connected-with x
    proof
      let o be Object of C;
      assume o in O2;
      then o in O9 by XBOOLE_0:def 3;
      hence thesis by A6;
    end;
    then x in {a where a is Attribute of C : for o being Object of C st o in
    O2 holds o is-connected-with a};
    then
A7: x in (ObjectDerivation(C)).O2 by Def2;
    for o being Object of C st o in O1 holds o is-connected-with x
    proof
      let o be Object of C;
      assume o in O1;
      then o in O9 by XBOOLE_0:def 3;
      hence thesis by A6;
    end;
    then
    x in {a where a is Attribute of C : for o being Object of C st o in O1
    holds o is-connected-with a};
    then x in (ObjectDerivation(C)).O1 by Def2;
    hence thesis by A7,XBOOLE_0:def 4;
  end;
  hence thesis by A1,TARSKI:2;
end;

theorem Th16:
  for C being FormalContext for A1,A2 being Subset of the carrier'
of C holds (AttributeDerivation(C)).(A1 \/ A2) = ((AttributeDerivation(C)).A1)
  /\ ((AttributeDerivation(C)).A2)
proof
  let C be FormalContext;
  let A1,A2 be Subset of the carrier' of C;
  reconsider A9 = A1 \/ A2 as Subset of the carrier' of C;
A1: for x being object holds x in (AttributeDerivation(C)).A1 /\ (
  AttributeDerivation(C)).A2 implies x in (AttributeDerivation(C)).A9
  proof
    let x be object;
    assume
A2: x in (AttributeDerivation(C)).A1 /\ (AttributeDerivation(C)).A2;
    then x in (AttributeDerivation(C)).A1 by XBOOLE_0:def 4;
    then x in {o where o is Object of C : for a being Attribute of C st a in
    A1 holds o is-connected-with a} by Def3;
    then
A3: ex x1 being Object of C st x1 = x & for a being Attribute of C st a in
    A1 holds x1 is-connected-with a;
    x in (AttributeDerivation(C)).A2 by A2,XBOOLE_0:def 4;
    then x in {o where o is Object of C : for a being Attribute of C st a in
    A2 holds o is-connected-with a} by Def3;
    then
A4: ex x2 being Object of C st x2 = x & for a being Attribute of C st a in
    A2 holds x2 is-connected-with a;
    then reconsider x as Object of C;
    for a being Attribute of C st a in A1 \/ A2 holds x is-connected-with a
    proof
      let a be Attribute of C;
      assume
A5:   a in (A1 \/ A2);
      now
        per cases by A5,XBOOLE_0:def 3;
        case
          a in A1;
          hence thesis by A3;
        end;
        case
          a in A2;
          hence thesis by A4;
        end;
      end;
      hence thesis;
    end;
    then x in {o where o is Object of C : for a being Attribute of C st a in
    A9 holds o is-connected-with a};
    hence thesis by Def3;
  end;
  for x being object holds x in (AttributeDerivation(C)).(A1 \/ A2) implies x
  in (AttributeDerivation(C)).A1 /\ (AttributeDerivation(C)).A2
  proof
    let x be object;
    assume x in (AttributeDerivation(C)).(A1 \/ A2);
    then
    x in {o where o is Object of C : for a being Attribute of C st a in A9
    holds o is-connected-with a} by Def3;
    then
A6: ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    A9 holds x9 is-connected-with a;
    then reconsider x as Object of C;
    for a being Attribute of C st a in A2 holds x is-connected-with a
    proof
      let a be Attribute of C;
      assume a in A2;
      then a in A9 by XBOOLE_0:def 3;
      hence thesis by A6;
    end;
    then x in {o where o is Object of C : for a being Attribute of C st a in
    A2 holds o is-connected-with a};
    then
A7: x in (AttributeDerivation(C)).A2 by Def3;
    for a being Attribute of C st a in A1 holds x is-connected-with a
    proof
      let a be Attribute of C;
      assume a in A1;
      then a in A9 by XBOOLE_0:def 3;
      hence thesis by A6;
    end;
    then
    x in {o where o is Object of C : for a being Attribute of C st a in A1
    holds o is-connected-with a};
    then x in (AttributeDerivation(C)).A1 by Def3;
    hence thesis by A7,XBOOLE_0:def 4;
  end;
  hence thesis by A1,TARSKI:2;
end;

theorem Th17:
  for C being FormalContext holds (ObjectDerivation(C)).{} = the carrier' of C
proof
  let C be FormalContext;
  reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
  set A = {a where a is Attribute of C : for o being Object of C st o in e
  holds o is-connected-with a};
A1: for x being object holds x in A implies x in the carrier' of C
  proof
    let x be object;
    assume x in A;
    then
    ex x9 being Attribute of C st x9 = x & for o being Object of C st o in
    e holds o is-connected-with x9;
    hence thesis;
  end;
A2: for x being object holds x in the carrier' of C implies x in A
  proof
    let x be object;
    assume x in the carrier' of C;
    then reconsider x as Attribute of C;
    for o being Object of C st o in e holds o is-connected-with x;
    hence thesis;
  end;
  (ObjectDerivation(C)).e = {a where a is Attribute of C : for o being
  Object of C st o in e holds o is-connected-with a} by Def2;
  hence thesis by A1,A2,TARSKI:2;
end;

theorem Th18:
  for C being FormalContext holds (AttributeDerivation(C)).{} =
  the carrier of C
proof
  let C be FormalContext;
  reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
  set O = {o where o is Object of C : for a being Attribute of C st a in e
  holds o is-connected-with a};
A1: for x being object holds x in O implies x in the carrier of C
  proof
    let x be object;
    assume x in O;
    then
    ex x9 being Object of C st x9 = x & for a being Attribute of C st a in
    e holds x9 is-connected-with a;
    hence thesis;
  end;
A2: for x being object holds x in the carrier of C implies x in O
  proof
    let x be object;
    assume x in the carrier of C;
    then reconsider x as Object of C;
    for a being Attribute of C st a in e holds x is-connected-with a;
    hence thesis;
  end;
  (AttributeDerivation(C)).e = {o where o is Object of C : for a being
  Attribute of C st a in e holds o is-connected-with a} by Def3;
  hence thesis by A1,A2,TARSKI:2;
end;

begin :: Formal Concepts

definition
  let C be 2-sorted;
  struct ConceptStr over C (# Extent -> Subset of the carrier of C, Intent ->
    Subset of the carrier' of C #);
end;

definition
  let C be 2-sorted;
  let CP be ConceptStr over C;
  attr CP is empty means
  :Def7:
  the Extent of CP is empty & the Intent of CP is empty;
  attr CP is quasi-empty means
  :Def8:
  the Extent of CP is empty or the Intent of CP is empty;
end;

registration
  let C be non empty non void 2-sorted;
  cluster strict non empty for ConceptStr over C;
  existence
  proof
    set A = the non empty Subset of the carrier' of C;
    set O = the non empty Subset of the carrier of C;
    ConceptStr(#O,A#) is non empty;
    hence thesis;
  end;
  cluster strict quasi-empty for ConceptStr over C;
  existence
  proof
    reconsider A = {} as Subset of the carrier' of C by XBOOLE_1:2;
    reconsider O = {} as Subset of the carrier of C by XBOOLE_1:2;
    ConceptStr(#O,A#) is quasi-empty;
    hence thesis;
  end;
end;

registration
  let C be empty void 2-sorted;
  cluster -> empty for ConceptStr over C;
  coherence;
end;

Lm1: for C being FormalContext for CS being ConceptStr over C st (
ObjectDerivation(C)).(the Extent of CS) = the Intent of CS holds CS is non
empty
proof
  let C be FormalContext;
  let CS be ConceptStr over C;
  assume
A1: (ObjectDerivation(C)).(the Extent of CS) = the Intent of CS;
  now
    per cases;
    case
      the Extent of CS is empty;
      then the Intent of CS = the carrier' of C by A1,Th17;
      hence thesis;
    end;
    case
      the Extent of CS is non empty;
      hence thesis;
    end;
  end;
  hence thesis;
end;

definition
  let C be FormalContext;
  let CP be ConceptStr over C;
  attr CP is concept-like means
  :Def9:
  (ObjectDerivation(C)).(the Extent of
  CP) = the Intent of CP & (AttributeDerivation(C)).(the Intent of CP) = the
  Extent of CP;
end;

registration
  let C be FormalContext;
  cluster concept-like non empty for ConceptStr over C;
  existence
  proof
    set o = the Object of C;
    set A = (ObjectDerivation(C)).({o});
    {o} c= the carrier of C
    proof
      let x be object;
      assume x in {o};
      then x = o by TARSKI:def 1;
      hence thesis;
    end;
    then reconsider t = {o} as Subset of the carrier of C;
    A c= the carrier' of C
    proof
      let x be object;
      assume x in A;
      then
      x in {a where a is Attribute of C : for o being Object of C st o in
      t holds o is-connected-with a} by Def2;
      then ex x9 being Attribute of C st x9 = x & for o being Object of C st o
      in t holds o is-connected-with x9;
      hence thesis;
    end;
    then reconsider A as Subset of the carrier' of C;
    set O = (AttributeDerivation(C)).((ObjectDerivation(C)).({o}));
    O c= the carrier of C
    proof
      let x be object;
      assume x in O;
      then x in {o9 where o9 is Object of C : for a being Attribute of C st a
      in ((ObjectDerivation(C)).t) holds o9 is-connected-with a} by Def3;
      then ex x9 being Object of C st x9 = x & for a being Attribute of C st a
      in ((ObjectDerivation(C)).t) holds x9 is-connected-with a;
      hence thesis;
    end;
    then reconsider O as Subset of the carrier of C;
    set M9 = ConceptStr(#O,A#);
    o in {o} & t c= (AttributeDerivation(C)).((ObjectDerivation(C)).t) by Th5,
TARSKI:def 1;
    then reconsider M9 as non empty ConceptStr over C by Def7;
    (ObjectDerivation(C)).(the Extent of M9) = (ObjectDerivation(C)).t by Th7
      .= the Intent of M9;
    then M9 is concept-like;
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  mode FormalConcept of C is concept-like non empty ConceptStr over C;
end;

registration
  let C be FormalContext;
  cluster strict for FormalConcept of C;
  existence
  proof
    set CP = the FormalConcept of C;
A1: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & (
    AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
    the Intent of CP is non empty or the Extent of CP is non empty by Def7;
    then the ConceptStr of CP is FormalConcept of C by A1,Def7,Def9;
    hence thesis;
  end;
end;

theorem Th19:
  for C being FormalContext for O being Subset of the carrier of C
  holds ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), (
    ObjectDerivation(C)).O#) is FormalConcept of C & for O9 being Subset of the
  carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is
FormalConcept of C & O c= O9 holds (AttributeDerivation(C)).((ObjectDerivation(
  C)).O) c= O9
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
A1: for O9 being Subset of the carrier of C, A9 being Subset of the carrier'
  of C st ConceptStr(#O9,A9#) is FormalConcept of C & O c= O9 holds (
  AttributeDerivation(C)).((ObjectDerivation(C)).O) c= O9
  proof
    let O9 be Subset of the carrier of C;
    let A9 be Subset of the carrier' of C;
    assume that
A2: ConceptStr(#O9,A9#) is FormalConcept of C and
A3: O c= O9;
    reconsider M9 = ConceptStr(#O9,A9#) as FormalConcept of C by A2;
A4: (AttributeDerivation(C)).(A9) = the Extent of M9 by Def9
      .= O9;
A5: (ObjectDerivation(C)).(O9) = the Intent of M9 by Def9
      .= A9;
    (ObjectDerivation(C)).(O9) c= (ObjectDerivation(C)).(O) by A3,Th3;
    hence thesis by A4,A5,Th4;
  end;
  ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), (
    ObjectDerivation(C)).O#) is FormalConcept of C
  proof
    set M9 = ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), (
      ObjectDerivation(C)).O#);
    (ObjectDerivation(C)).(the Extent of M9) = the Intent of M9 by Th7;
    hence thesis by Def9,Lm1;
  end;
  hence thesis by A1;
end;

theorem
  for C being FormalContext for O being Subset of the carrier of C holds
  (ex A being Subset of the carrier' of C st ConceptStr(#O,A#) is FormalConcept
  of C) iff (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O
proof
  let C be FormalContext;
  let O be Subset of the carrier of C;
A1: now
    O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O) by Th5;
    then
A2: for x being object holds x in O implies x in (AttributeDerivation(C)).((
    ObjectDerivation(C)).O);
    given A being Subset of the carrier' of C such that
A3: ConceptStr(#O,A#) is FormalConcept of C;
    (AttributeDerivation(C)).((ObjectDerivation(C)).O) c= O by A3,Th19;
    then
    for x being object holds x in (AttributeDerivation(C)).((ObjectDerivation
    (C)).O) implies x in O;
    hence (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O by A2,TARSKI:2
;
  end;
  now
    reconsider A = (ObjectDerivation(C)).O as Subset of the carrier' of C;
    set M9 = ConceptStr(#O,A#);
    assume (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O;
    then M9 is FormalConcept of C by Def9,Lm1;
    hence ex A being Subset of the carrier' of C st ConceptStr(#O,A#) is
    FormalConcept of C;
  end;
  hence thesis by A1;
end;

theorem Th21:
  for C being FormalContext for A being Subset of the carrier' of
  C holds ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).((
AttributeDerivation(C)).A)#) is FormalConcept of C & for O9 being Subset of the
  carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is
FormalConcept of C & A c= A9 holds (ObjectDerivation(C)).((AttributeDerivation(
  C)).A) c= A9
proof
  let C be FormalContext;
  let A be Subset of the carrier' of C;
A1: for O9 being Subset of the carrier of C, A9 being Subset of the carrier'
  of C st ConceptStr(#O9,A9#) is FormalConcept of C & A c= A9 holds (
  ObjectDerivation(C)).((AttributeDerivation(C)).A) c= A9
  proof
    let O9 be Subset of the carrier of C;
    let A9 be Subset of the carrier' of C;
    assume that
A2: ConceptStr(#O9,A9#) is FormalConcept of C and
A3: A c= A9;
    reconsider M9 = ConceptStr(#O9,A9#) as FormalConcept of C by A2;
A4: (AttributeDerivation(C)).(A9) = the Extent of M9 by Def9
      .= O9;
A5: (ObjectDerivation(C)).(O9) = the Intent of M9 by Def9
      .= A9;
    (AttributeDerivation(C)).(A9) c= (AttributeDerivation(C)).(A) by A3,Th4;
    hence thesis by A4,A5,Th3;
  end;
  ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).((
    AttributeDerivation(C)).A)#) is FormalConcept of C
  proof
    set M9 = ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).((
      AttributeDerivation(C)).A)#);
    (AttributeDerivation(C)).(the Intent of M9) = the Extent of M9 by Th8;
    hence thesis by Def9,Lm1;
  end;
  hence thesis by A1;
end;

theorem
  for C being FormalContext for A being Subset of the carrier' of C
  holds (ex O being Subset of the carrier of C st ConceptStr(#O,A#) is
FormalConcept of C) iff (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A
proof
  let C be FormalContext;
  let A be Subset of the carrier' of C;
A1: now
    A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A) by Th6;
    then
A2: for x being object holds x in A implies x in (ObjectDerivation(C)).((
    AttributeDerivation(C)).A);
    given O being Subset of the carrier of C such that
A3: ConceptStr(#O,A#) is FormalConcept of C;
    (ObjectDerivation(C)).((AttributeDerivation(C)).A) c= A by A3,Th21;
    then
    for x being object holds x in (ObjectDerivation(C)).((AttributeDerivation
    (C)).A) implies x in A;
    hence (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A by A2,TARSKI:2
;
  end;
  now
    reconsider O = (AttributeDerivation(C)).A as Subset of the carrier of C;
    set M9 = ConceptStr(#O,A#);
    assume (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A;
    then M9 is FormalConcept of C by Def9,Lm1;
    hence ex O being Subset of the carrier of C st ConceptStr(#O,A#) is
    FormalConcept of C;
  end;
  hence thesis by A1;
end;

definition
  let C be FormalContext;
  let CP be ConceptStr over C;
  attr CP is universal means

  the Extent of CP = the carrier of C;
end;

definition
  let C be FormalContext;
  let CP be ConceptStr over C;
  attr CP is co-universal means

  the Intent of CP = the carrier' of C;
end;

registration
  let C be FormalContext;
  cluster strict universal for FormalConcept of C;
  existence
  proof
    reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
    reconsider CP = ConceptStr(#(AttributeDerivation(C)).(e), (
ObjectDerivation(C)).((AttributeDerivation(C)).(e))#) as FormalConcept of C by
Th21;
    (AttributeDerivation(C)).({}) = the carrier of C by Th18;
    then CP is universal;
    hence thesis;
  end;
  cluster strict co-universal for FormalConcept of C;
  existence
  proof
    reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
    reconsider CP = ConceptStr(# (AttributeDerivation(C)).((ObjectDerivation(C
      )).(e)), (ObjectDerivation(C)).(e)#) as FormalConcept of C by Th19;
    (ObjectDerivation(C)).({}) = the carrier' of C by Th17;
    then CP is co-universal;
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  func Concept-with-all-Objects(C) -> strict universal FormalConcept of C
  means
  :Def12:
  ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).({}) & A
  = (ObjectDerivation(C)).((AttributeDerivation(C)).({}));
  existence
  proof
    reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
    reconsider CP = ConceptStr(#(AttributeDerivation(C)).(e), (
ObjectDerivation(C)).((AttributeDerivation(C)).(e))#) as FormalConcept of C by
Th21;
    (AttributeDerivation(C)).({}) = the carrier of C by Th18;
    then CP is universal;
    hence thesis;
  end;
  uniqueness;
end;

definition
  let C be FormalContext;
  func Concept-with-all-Attributes(C) -> strict co-universal FormalConcept of
  C means
  :Def13:
  ex O being Subset of the carrier of C, A being Subset of the
  carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((
  ObjectDerivation(C)).({})) & A = (ObjectDerivation(C)).({});
  existence
  proof
    reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
    reconsider CP = ConceptStr(# (AttributeDerivation(C)).((ObjectDerivation(C
      )).(e)), (ObjectDerivation(C)).(e)#) as FormalConcept of C by Th19;
    (ObjectDerivation(C)).({}) = the carrier' of C by Th17;
    then CP is co-universal;
    hence thesis;
  end;
  uniqueness;
end;

theorem Th23:
  for C being FormalContext holds the Extent of
  Concept-with-all-Objects(C) = the carrier of C & the Intent of
  Concept-with-all-Attributes(C) = the carrier' of C
proof
  let C be FormalContext;
  (ex O being Subset of the carrier of C, A being Subset of the carrier'
  of C st Concept-with-all-Objects(C) = ConceptStr(#O,A#) & O = (
AttributeDerivation(C) ).({}) & A = (ObjectDerivation(C)).((AttributeDerivation
  (C)).({})) )& ex O being Subset of the carrier of C, A being Subset of the
  carrier' of C st Concept-with-all-Attributes(C) = ConceptStr(#O,A#) & O = (
AttributeDerivation( C)).((ObjectDerivation(C)).({})) & A = ( ObjectDerivation(
  C)).({}) by Def12,Def13;
  hence thesis by Th17,Th18;
end;

theorem
  for C being FormalContext for CP being FormalConcept of C holds (the
Extent of CP = {} implies CP is co-universal) & (the Intent of CP = {} implies
  CP is universal)
proof
  let C be FormalContext;
  let CP be FormalConcept of C;
A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
A2: the Intent of CP = {} implies CP is universal by A1,Th18;
A3: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9;
   the Extent of CP = {} implies CP is co-universal by A3,Th17;
  hence thesis by A2;
end;

theorem Th25:
  for C being FormalContext for CP being strict FormalConcept of C
  holds (the Extent of CP = {} implies CP = Concept-with-all-Attributes(C)) & (
  the Intent of CP = {} implies CP = Concept-with-all-Objects(C))
proof
  let C be FormalContext;
  let CP be strict FormalConcept of C;
A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
A2: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9;
A3: now
    assume
A4: the Intent of CP = {};
    then the Extent of CP = the carrier of C by A1,Th18;
    then CP is universal;
    hence CP = Concept-with-all-Objects(C) by A2,A1,A4,Def12;
  end;
  now
    assume
A5: the Extent of CP = {};
    then the Intent of CP = the carrier' of C by A2,Th17;
    then CP is co-universal;
    hence CP = Concept-with-all-Attributes(C) by A2,A1,A5,Def13;
  end;
  hence thesis by A3;
end;

theorem
  for C being FormalContext for CP being quasi-empty ConceptStr over C
  st CP is FormalConcept of C holds CP is universal or CP is co-universal
proof
  let C be FormalContext;
  let CP be quasi-empty ConceptStr over C;
  assume CP is FormalConcept of C;
  then reconsider CP as FormalConcept of C;
A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
A2: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9;
  now
    per cases by Def8;
    case
      the Intent of CP is empty;
      then the Extent of CP = the carrier of C by A1,Th18;
      hence CP is universal;
    end;
    case
      the Extent of CP is empty;
      then the Intent of CP = the carrier' of C by A2,Th17;
      hence CP is co-universal;
    end;
  end;
  hence thesis;
end;

theorem
  for C being FormalContext for CP being quasi-empty ConceptStr over C
st CP is strict FormalConcept of C holds CP = Concept-with-all-Objects(C) or CP
  = Concept-with-all-Attributes(C)
proof
  let C be FormalContext;
  let CP be quasi-empty ConceptStr over C;
  assume
A1: CP is strict FormalConcept of C;
  now
    per cases by Def8;
    case
      the Intent of CP is empty;
      hence CP = Concept-with-all-Objects(C) by A1,Th25;
    end;
    case
      the Extent of CP is empty;
      hence CP = Concept-with-all-Attributes(C) by A1,Th25;
    end;
  end;
  hence thesis;
end;

definition
  let C be FormalContext;
  mode Set-of-FormalConcepts of C -> non empty set means
    :Def14:
    for X being set st X in it holds X is FormalConcept of C;
  existence
  proof
    set CP = the FormalConcept of C;
    for X being set st X in {CP} holds X is FormalConcept of C by TARSKI:def 1;
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  let FCS be Set-of-FormalConcepts of C;
  redefine mode Element of FCS -> FormalConcept of C;
  coherence by Def14;
end;

definition
  let C be FormalContext;
  let CP1,CP2 be FormalConcept of C;
  pred CP1 is-SubConcept-of CP2 means

  the Extent of CP1 c= the Extent of CP2;
end;

notation
  let C be FormalContext;
  let CP1,CP2 be FormalConcept of C;
  synonym CP2 is-SuperConcept-of CP1 for CP1 is-SubConcept-of CP2;
end;

theorem Th28:
  for C being FormalContext for CP1,CP2 being FormalConcept of C
  holds CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1
proof
  let C be FormalContext;
  let CP1,CP2 be FormalConcept of C;
A1: now
    assume the Intent of CP2 c= the Intent of CP1;
    then
A2: (AttributeDerivation(C)).(the Intent of CP1) c= (AttributeDerivation(C
    )).(the Intent of CP2) by Th4;
    (AttributeDerivation(C)).(the Intent of CP1) = the Extent of CP1 & (
    AttributeDerivation(C)).(the Intent of CP2) = the Extent of CP2 by Def9;
    hence CP1 is-SubConcept-of CP2 by A2;
  end;
  now
    assume CP1 is-SubConcept-of CP2;
    then
A3: the Extent of CP1 c= the Extent of CP2;
    (ObjectDerivation(C)).(the Extent of CP2) = the Intent of CP2 & (
    ObjectDerivation(C)).(the Extent of CP1) = the Intent of CP1 by Def9;
    hence the Intent of CP2 c= the Intent of CP1 by A3,Th3;
  end;
  hence thesis by A1;
end;

theorem
  for C being FormalContext for CP1,CP2 being FormalConcept of C holds
CP1 is-SuperConcept-of CP2 iff the Intent of CP1 c= the Intent of CP2 by Th28;

theorem
  for C being FormalContext for CP being FormalConcept of C holds CP
  is-SubConcept-of Concept-with-all-Objects(C) & Concept-with-all-Attributes(C)
  is-SubConcept-of CP
proof
  let C be FormalContext;
  let CP be FormalConcept of C;
A1: the carrier' of C = the Intent of Concept-with-all-Attributes(C) & the
  Intent of CP c= the carrier' of C by Th23;
  the carrier of C = the Extent of Concept-with-all-Objects(C) & the
  Extent of CP c= the carrier of C by Th23;
  hence thesis by A1,Th28;
end;

begin :: Concept Lattices

definition
  let C be FormalContext;
  func B-carrier(C) -> non empty set equals
  { ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) is non empty & (ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E
  };
  coherence
  proof
    set M9 = { ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
    Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & (
    ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E };
    M9 is non empty
    proof
      set CP = the FormalConcept of C;
      consider O being Subset of the carrier of C such that
A1:   O = the Extent of CP;
      consider A being Subset of the carrier' of C such that
A2:   A = the Intent of CP;
A3:   (AttributeDerivation(C)).A = O by A1,A2,Def9;
A4:   (ObjectDerivation(C)).O = A by A1,A2,Def9;
      then ConceptStr(#O,A#) is non empty by Lm1;
      then ConceptStr(#O,A#) in M9 by A4,A3;
      hence thesis;
    end;
    then reconsider M9 as non empty set;
    for CP being strict non empty ConceptStr over C holds CP in M9 iff (
    ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & (
    AttributeDerivation(C)).(the Intent of CP) = the Extent of CP
    proof
      let CP be strict non empty ConceptStr over C;
      now
        assume CP in M9;
        then ex E being Subset of the carrier of C, I being Subset of the
carrier' of C st CP = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & (
        ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E;
        hence (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & (
        AttributeDerivation(C)).(the Intent of CP) = the Extent of CP;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  redefine func B-carrier(C) -> Set-of-FormalConcepts of C;
  coherence
  proof
    for X being set holds X in B-carrier(C) implies X is FormalConcept of C
    proof
      let X be set;
      assume X in B-carrier(C);
      then
      ex E being Subset of the carrier of C, I being Subset of the carrier'
      of C st X = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & (
      ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E;
      hence thesis by Def9;
    end;
    hence thesis by Def14;
  end;
end;

registration
  let C be FormalContext;
  cluster B-carrier(C) -> non empty;
  coherence;
end;

theorem Th31:
  for C being FormalContext for CP being object holds CP in B-carrier
  (C) iff CP is strict FormalConcept of C
proof
  let C be FormalContext;
  let CP be object;
A1: CP is strict FormalConcept of C implies CP in B-carrier(C)
  proof
    assume
A2: CP is strict FormalConcept of C;
    then reconsider CP as FormalConcept of C;
    set I9 = the Intent of CP;
    set E9 = the Extent of CP;
    (ObjectDerivation(C)).E9 = I9 & (AttributeDerivation(C)).I9 = E9 by Def9;
    hence thesis by A2;
  end;
  CP in B-carrier(C) implies CP is strict FormalConcept of C
  proof
    assume CP in B-carrier(C);
    then ex E being Subset of the carrier of C, I being Subset of the carrier'
    of C st CP = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & (
    ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E;
    hence thesis by Def9;
  end;
  hence thesis by A1;
end;

definition
  let C be FormalContext;
  func B-meet(C) -> BinOp of B-carrier(C) means
  :Def17:
  for CP1,CP2 being
strict FormalConcept of C holds ex O being Subset of the carrier of C, A being
  Subset of the carrier' of C st it.(CP1,CP2) = ConceptStr(#O,A#) & O = (the
  Extent of CP1) /\ (the Extent of CP2) & A = (ObjectDerivation(C)).((
  AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2)));
  existence
  proof
    defpred P[FormalConcept of C, FormalConcept of C, set] means ex O being
    Subset of the carrier of C, A being Subset of the carrier' of C st ($3 =
    ConceptStr(#O,A#) & O = (the Extent of $1) /\ (the Extent of $2) & A = (
    ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of $1) \/ (the
    Intent of $2))));
A1: for CP1 being Element of B-carrier(C), CP2 being Element of B-carrier(
    C) ex CP being Element of B-carrier(C) st P[CP1,CP2,CP]
    proof
      let CP1 be Element of B-carrier(C);
      let CP2 be Element of B-carrier(C);
      set O = (the Extent of CP1) /\ (the Extent of CP2);
      set A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of
      CP1) \/ (the Intent of CP2)));
      reconsider A9 = (the Intent of CP1) \/ (the Intent of CP2) as Subset of
      the carrier' of C;
      set CP = ConceptStr(#O,A#);
A2:   (AttributeDerivation(C)).A = (AttributeDerivation(C)).A9 by Th8
        .= (AttributeDerivation(C)).(the Intent of CP1) /\ (
      AttributeDerivation(C)).(the Intent of CP2) by Th16
        .= (the Extent of CP1) /\ (AttributeDerivation(C)).(the Intent of
      CP2) by Def9
        .= (the Extent of CP1) /\ (the Extent of CP2) by Def9;
      then
A3:   (ObjectDerivation(C)).O = A by Th7;
      then ConceptStr(#O,A#) is non empty by Lm1;
      then
      CP in {ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
      Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & (
      ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E } by A2,A3;
      hence thesis;
    end;
    consider f being Function of [:B-carrier(C),B-carrier(C):],B-carrier(C)
    such that
A4: for CP1 being Element of B-carrier(C), CP2 being Element of
    B-carrier(C) holds P[CP1,CP2,f.(CP1,CP2)] from BINOP_1:sch 3(A1);
    reconsider f as BinOp of B-carrier(C);
    take f;
    for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of
    the carrier of C, A being Subset of the carrier' of C st f.(CP1,CP2) =
    ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (
ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the
    Intent of CP2)))
    proof
      let CP1,CP2 be strict FormalConcept of C;
      CP1 is Element of B-carrier(C) & CP2 is Element of B-carrier(C) by Th31;
      hence thesis by A4;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let F1,F2 be BinOp of B-carrier(C);
    assume
A5: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, A being Subset of the carrier' of C st F1.(CP1,CP2)
= ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (
ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the
    Intent of CP2)));
    assume
A6: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, A being Subset of the carrier' of C st F2.(CP1,CP2)
= ConceptStr(#O,A#) & O = (the Extent of CP1) /\ (the Extent of CP2) & A = (
ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the
    Intent of CP2)));
A7: for X being object st X in [:B-carrier(C),B-carrier(C):]
   holds F1.X = F2 .X
    proof
      let X be object;
      assume X in [:B-carrier(C),B-carrier(C):];
      then consider A,B being object such that
A8:   A in B-carrier(C) and
A9:   B in B-carrier(C) and
A10:  X = [A,B] by ZFMISC_1:def 2;
      reconsider B as strict FormalConcept of C by A9,Th31;
      reconsider A as strict FormalConcept of C by A8,Th31;
      (ex O being Subset of the carrier of C, At being Subset of the
carrier' of C st F1.(A,B) = ConceptStr(#O,At#) & O = (the Extent of A) /\ (the
Extent of B) & At = (ObjectDerivation(C)).((AttributeDerivation(C)). ( (the
Intent of A) \/ ( the Intent of B))) )& ex O9 being Subset of the carrier of C,
At9 being Subset of the carrier' of C st F2.(A,B) = ConceptStr(#O9,At9#) & O9 =
      (the Extent of A ) /\ (the Extent of B) & At9 = (ObjectDerivation(C)).((
AttributeDerivation(C)) . ((the Intent of A) \/ (the Intent of B))) by A5,A6;
      hence thesis by A10;
    end;
    dom F1 = [:B-carrier(C),B-carrier(C):] & dom F2 = [:B-carrier(C),
    B-carrier(C ):] by FUNCT_2:def 1;
    hence thesis by A7,FUNCT_1:2;
  end;
end;

definition
  let C be FormalContext;
  func B-join(C) -> BinOp of B-carrier(C) means
  :Def18:
  for CP1,CP2 being
strict FormalConcept of C holds ex O being Subset of the carrier of C, A being
  Subset of the carrier' of C st it.(CP1,CP2) = ConceptStr(#O,A#) & O = (
  AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the
  Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2);
  existence
  proof
    defpred P[FormalConcept of C, FormalConcept of C, set] means ex O being
    Subset of the carrier of C, A being Subset of the carrier' of C st ($3 =
ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the
Extent of $1) \/ (the Extent of $2))) & A = (the Intent of $1) /\ (the Intent
    of $2));
A1: for CP1 being Element of B-carrier(C), CP2 being Element of B-carrier(
    C) ex CP being Element of B-carrier(C) st P[CP1,CP2,CP]
    proof
      let CP1 be Element of B-carrier(C);
      let CP2 be Element of B-carrier(C);
      set O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of
      CP1) \/ (the Extent of CP2)));
      set A = (the Intent of CP1) /\ (the Intent of CP2);
      reconsider O9 = (the Extent of CP1) \/ (the Extent of CP2) as Subset of
      the carrier of C;
      set CP = ConceptStr(#O,A#);
A2:   (ObjectDerivation(C)).O = (ObjectDerivation(C)).O9 by Th7
        .= (ObjectDerivation(C)).(the Extent of CP1) /\ (ObjectDerivation(C)
      ).(the Extent of CP2) by Th15
        .= (the Intent of CP1) /\ (ObjectDerivation(C)).(the Extent of CP2)
      by Def9
        .= (the Intent of CP1) /\ (the Intent of CP2) by Def9;
      then (AttributeDerivation(C)).A = O & ConceptStr(#O,A#) is non empty by
Lm1,Th7;
      then
      CP in {ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
      Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & (
      ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E } by A2;
      hence thesis;
    end;
    consider f being Function of [:B-carrier(C),B-carrier(C):],B-carrier(C)
    such that
A3: for CP1 being Element of B-carrier(C), CP2 being Element of
    B-carrier(C) holds P[CP1,CP2,f.(CP1,CP2)] from BINOP_1:sch 3(A1);
    reconsider f as BinOp of B-carrier(C);
    take f;
    for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of
    the carrier of C, A being Subset of the carrier' of C st f.(CP1,CP2) =
ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the
    Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the
    Intent of CP2)
    proof
      let CP1,CP2 be strict FormalConcept of C;
      CP1 is Element of B-carrier(C) & CP2 is Element of B-carrier(C) by Th31;
      hence thesis by A3;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let F1,F2 be BinOp of B-carrier(C);
    assume
A4: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, A being Subset of the carrier' of C st F1.(CP1,CP2)
= ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((
the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the
    Intent of CP2);
    assume
A5: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, A being Subset of the carrier' of C st F2.(CP1,CP2)
= ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((
the Extent of CP1) \/ (the Extent of CP2))) & A = (the Intent of CP1) /\ (the
    Intent of CP2);
A6: for X being object st X in [:B-carrier(C),B-carrier(C):]
holds F1.X = F2 .X
    proof
      let X be object;
      assume X in [:B-carrier(C),B-carrier(C):];
      then consider A,B being object such that
A7:   A in B-carrier(C) and
A8:   B in B-carrier(C) and
A9:   X = [A,B] by ZFMISC_1:def 2;
      reconsider B as strict FormalConcept of C by A8,Th31;
      reconsider A as strict FormalConcept of C by A7,Th31;
      (ex O being Subset of the carrier of C, At being Subset of the
carrier' of C st F1.(A,B) = ConceptStr(#O,At#) & O = ( AttributeDerivation(C)).
(( ObjectDerivation(C)). ((the Extent of A) \/ (the Extent of B))) & At = (the
Intent of A) /\ (the Intent of B) )& ex O9 being Subset of the carrier of C,
At9 being Subset of the carrier' of C st F2.(A,B) = ConceptStr(#O9,At9#) & O9 =
( AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of A) \/ ( the
      Extent of B))) & At9 = (the Intent of A) /\ (the Intent of B) by A4,A5;
      hence thesis by A9;
    end;
    dom F1 = [:B-carrier(C),B-carrier(C):] & dom F2 = [:B-carrier(C),
    B-carrier(C ):] by FUNCT_2:def 1;
    hence thesis by A6,FUNCT_1:2;
  end;
end;

Lm2: for C being FormalContext for CP1,CP2 being strict FormalConcept of C
holds (B-meet(C)).(CP1,CP2) in rng((B-meet(C)))
proof
  let C be FormalContext;
  let CP1,CP2 be strict FormalConcept of C;
  CP1 in B-carrier(C) & CP2 in B-carrier(C) by Th31;
  then [CP1,CP2] in [:B-carrier(C),B-carrier(C):] by ZFMISC_1:def 2;
  then [CP1,CP2] in dom((B-meet(C))) by FUNCT_2:def 1;
  hence thesis by FUNCT_1:def 3;
end;

Lm3: for C being FormalContext for CP1,CP2 being strict FormalConcept of C
holds (B-join(C)).(CP1,CP2) in rng((B-join(C)))
proof
  let C be FormalContext;
  let CP1,CP2 be strict FormalConcept of C;
  CP1 in B-carrier(C) & CP2 in B-carrier(C) by Th31;
  then [CP1,CP2] in [:B-carrier(C),B-carrier(C):] by ZFMISC_1:def 2;
  then [CP1,CP2] in dom((B-join(C))) by FUNCT_2:def 1;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th32:
  for C being FormalContext for CP1,CP2 being strict FormalConcept
  of C holds (B-meet(C)).(CP1,CP2) = (B-meet(C)).(CP2,CP1)
proof
  let C be FormalContext;
  let CP1,CP2 be strict FormalConcept of C;
  (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-meet(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\
(the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). ((
  the Intent of CP1) \/ (the Intent of CP2))) )& ex O9 being Subset of the
  carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP2,CP1) =
ConceptStr (#O9,A9#) & O9 = (the Extent of CP2) /\ (the Extent of CP1) & A9 = (
  ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP2) \/ (the
  Intent of CP1))) by Def17;
  hence thesis;
end;

theorem Th33:
  for C being FormalContext for CP1,CP2 being strict FormalConcept
  of C holds (B-join(C)).(CP1,CP2) = (B-join(C)).(CP2,CP1)
proof
  let C be FormalContext;
  let CP1,CP2 be strict FormalConcept of C;
  (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-join(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C
)).(( ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A =
(the Intent of CP1) /\ (the Intent of CP2) )& ex O9 being Subset of the carrier
  of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP2,CP1) =
ConceptStr (#O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). (
(the Extent of CP2) \/ (the Extent of CP1))) & A9 = (the Intent of CP2) /\ (the
  Intent of CP1) by Def18;
  hence thesis;
end;

theorem Th34:
  for C being FormalContext for CP1,CP2,CP3 being strict
FormalConcept of C holds (B-meet(C)).(CP1,(B-meet(C)).(CP2,CP3)) = (B-meet(C)).
  ((B-meet(C)).(CP1,CP2),CP3)
proof
  let C be FormalContext;
  let CP1,CP2,CP3 be strict FormalConcept of C;
  (B-meet(C)).(CP1,CP2) in rng((B-meet(C))) by Lm2;
  then reconsider CP = (B-meet(C)).(CP1,CP2) as strict FormalConcept of C by
Th31;
A1: (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-meet(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\
(the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). ((
  the Intent of CP1) \/ (the Intent of CP2))) )& ex O9 being Subset of the
  carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP,CP3) =
ConceptStr (#O9,A9#) & O9 = (the Extent of CP) /\ (the Extent of CP3) & A9 = (
  ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP) \/ (the
  Intent of CP3))) by Def17;
  (B-meet(C)).(CP2,CP3) in rng((B-meet(C))) by Lm2;
  then reconsider CP9 = (B-meet(C)).(CP2,CP3) as strict FormalConcept of C by
Th31;
A2: (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-meet(C)).(CP2,CP3) = ConceptStr(#O,A#) & O = (the Extent of CP2) /\
(the Extent of CP3) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). ((
  the Intent of CP2) \/ (the Intent of CP3))) )& ex O9 being Subset of the
  carrier of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP1,CP9) =
ConceptStr (#O9,A9#) & O9 = (the Extent of CP1) /\ (the Extent of CP9) & A9 = (
  ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP1) \/ (the
  Intent of CP9))) by Def17;
  (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/
((ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP2) \/ (the
  Intent of CP3)))))) = (ObjectDerivation(C)). (((AttributeDerivation(C)).(the
  Intent of CP1)) /\ ((AttributeDerivation(C)). ((ObjectDerivation(C)).((
  AttributeDerivation(C)). ((the Intent of CP2) \/ (the Intent of CP3)))))) by
Th16
    .= (ObjectDerivation(C)). (((AttributeDerivation(C)).(the Intent of CP1)
) /\ ((AttributeDerivation(C)). ((the Intent of CP2) \/ (the Intent of CP3))))
  by Th8
    .= (ObjectDerivation(C)). (((AttributeDerivation(C)).(the Intent of CP1)
) /\ (((AttributeDerivation(C)).(the Intent of CP2)) /\ ((AttributeDerivation(C
  )).(the Intent of CP3)))) by Th16
    .= (ObjectDerivation(C)). ((((AttributeDerivation(C)).(the Intent of CP1
)) /\ ((AttributeDerivation(C)).(the Intent of CP2))) /\ ((AttributeDerivation(
  C)).(the Intent of CP3))) by XBOOLE_1:16
    .= (ObjectDerivation(C)). (((AttributeDerivation(C)). ((the Intent of
CP1) \/ (the Intent of CP2)) /\ ((AttributeDerivation(C)).(the Intent of CP3)))
  ) by Th16
    .= (ObjectDerivation(C)). (((AttributeDerivation(C)). ((ObjectDerivation
(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))))
  /\ ((AttributeDerivation(C)).(the Intent of CP3)))) by Th8
    .= (ObjectDerivation(C)).((AttributeDerivation(C)). (((ObjectDerivation(
  C)).((AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2))))
  \/ (the Intent of CP3))) by Th16;
  hence thesis by A1,A2,XBOOLE_1:16;
end;

theorem Th35:
  for C being FormalContext for CP1,CP2,CP3 being strict
FormalConcept of C holds (B-join(C)).(CP1,(B-join(C)).(CP2,CP3)) = (B-join(C)).
  ((B-join(C)).(CP1,CP2),CP3)
proof
  let C be FormalContext;
  let CP1,CP2,CP3 be strict FormalConcept of C;
  (B-join(C)).(CP1,CP2) in rng((B-join(C))) by Lm3;
  then reconsider CP = (B-join(C)).(CP1,CP2) as strict FormalConcept of C by
Th31;
A1: (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-join(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C
)).(( ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A =
(the Intent of CP1) /\ (the Intent of CP2) )& ex O9 being Subset of the carrier
  of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP,CP3) =
ConceptStr(# O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). (
  (the Extent of CP) \/ (the Extent of CP3))) & A9 = (the Intent of CP) /\ (the
  Intent of CP3) by Def18;
  (B-join(C)).(CP2,CP3) in rng((B-join(C))) by Lm3;
  then reconsider CP9 = (B-join(C)).(CP2,CP3) as strict FormalConcept of C by
Th31;
A2: (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-join(C)).(CP2,CP3) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C
)).(( ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3))) & A =
(the Intent of CP2) /\ (the Intent of CP3) )& ex O9 being Subset of the carrier
  of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP1,CP9) =
ConceptStr (#O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). (
(the Extent of CP1) \/ (the Extent of CP9))) & A9 = (the Intent of CP1) /\ (the
  Intent of CP9) by Def18;
  (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/
((AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP2) \/ (the
  Extent of CP3)))))) = (AttributeDerivation(C)). (((ObjectDerivation(C)).(the
  Extent of CP1)) /\ ((ObjectDerivation(C)). ((AttributeDerivation(C)).((
ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3)))))) by Th15
    .= (AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1)
) /\ ((ObjectDerivation(C)). ((the Extent of CP2) \/ (the Extent of CP3)))) by
Th7
    .= (AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1)
  ) /\ (((ObjectDerivation(C)).(the Extent of CP2)) /\ ((ObjectDerivation(C)).(
  the Extent of CP3)))) by Th15
    .= (AttributeDerivation(C)). ((((ObjectDerivation(C)).(the Extent of CP1
)) /\ ((ObjectDerivation(C)).(the Extent of CP2))) /\ ((ObjectDerivation(C)).(
  the Extent of CP3))) by XBOOLE_1:16
    .= (AttributeDerivation(C)). (((ObjectDerivation(C)). ((the Extent of
  CP1) \/ (the Extent of CP2)) /\ ((ObjectDerivation(C)).(the Extent of CP3))))
  by Th15
    .= (AttributeDerivation(C)). (((ObjectDerivation(C)). ((
  AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the
  Extent of CP2)))) /\ ((ObjectDerivation(C)).(the Extent of CP3)))) by Th7
    .= (AttributeDerivation(C)).((ObjectDerivation(C)). (((
  AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the
  Extent of CP2)))) \/ (the Extent of CP3))) by Th15;
  hence thesis by A1,A2,XBOOLE_1:16;
end;

theorem Th36:
  for C being FormalContext for CP1,CP2 being strict FormalConcept
  of C holds (B-join(C)).((B-meet(C)).(CP1,CP2),CP2) = CP2
proof
  let C be FormalContext;
  let CP1,CP2 be strict FormalConcept of C;
A1: ((the Extent of CP1) /\ (the Extent of CP2)) c= (the Extent of CP2) by
XBOOLE_1:17;
  (B-meet(C)).(CP1,CP2) in rng((B-meet(C))) by Lm2;
  then reconsider CP9 = (B-meet(C)).(CP1,CP2) as strict FormalConcept of C by
Th31;
A2: (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-meet(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = (the Extent of CP1) /\
(the Extent of CP2) & A = (ObjectDerivation(C)).(( AttributeDerivation(C)). ((
  the Intent of CP1) \/ (the Intent of CP2))) )& ex O9 being Subset of the
  carrier of C, A9 being Subset of the carrier' of C st (B-join(C)).(CP9,CP2) =
ConceptStr (#O9,A9#) & O9 = ( AttributeDerivation(C)).((ObjectDerivation(C)). (
(the Extent of CP9) \/ (the Extent of CP2))) & A9 = (the Intent of CP9) /\ (the
  Intent of CP2) by Def17,Def18;
  (AttributeDerivation(C)).((ObjectDerivation(C)). (((the Extent of CP1)
/\ (the Extent of CP2)) \/ (the Extent of CP2))) = (AttributeDerivation(C)). ((
  (ObjectDerivation(C)).((the Extent of CP1) /\ (the Extent of CP2))) /\ ((
  ObjectDerivation(C)).(the Extent of CP2))) by Th15;
  then
A3: (AttributeDerivation(C)).((ObjectDerivation(C)). (((the Extent of CP1)
/\ (the Extent of CP2)) \/ (the Extent of CP2))) = (AttributeDerivation(C)).((
  ObjectDerivation(C)).(the Extent of CP2)) by A1,Th3,XBOOLE_1:28
    .= (AttributeDerivation(C)).(the Intent of CP2) by Def9
    .= the Extent of CP2 by Def9;
  ((ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1)
\/ (the Intent of CP2)))) /\ (the Intent of CP2) = ((ObjectDerivation(C)). (((
AttributeDerivation(C)).(the Intent of CP1)) /\ ((AttributeDerivation(C)).(the
  Intent of CP2)))) /\ (the Intent of CP2) by Th16
    .= ((ObjectDerivation(C)). ((the Extent of CP1) /\ ((AttributeDerivation
  (C)).(the Intent of CP2)))) /\ (the Intent of CP2) by Def9
    .= ((ObjectDerivation(C)). ((the Extent of CP1) /\ (the Extent of CP2)))
  /\ (the Intent of CP2) by Def9
    .= ((ObjectDerivation(C)). ((the Extent of CP1) /\ (the Extent of CP2)))
  /\ ((ObjectDerivation(C)).(the Extent of CP2)) by Def9
    .= (ObjectDerivation(C)).(the Extent of CP2) by A1,Th3,XBOOLE_1:28
    .= the Intent of CP2 by Def9;
  hence thesis by A2,A3;
end;

theorem Th37:
  for C being FormalContext for CP1,CP2 being strict FormalConcept
  of C holds (B-meet(C)).(CP1,(B-join(C)).(CP1,CP2)) = CP1
proof
  let C be FormalContext;
  let CP1,CP2 be strict FormalConcept of C;
A1: ((the Intent of CP1) /\ (the Intent of CP2)) c= (the Intent of CP1) by
XBOOLE_1:17;
  (B-join(C)).(CP1,CP2) in rng((B-join(C))) by Lm3;
  then reconsider CP9 = (B-join(C)).(CP1,CP2) as strict FormalConcept of C by
Th31;
A2: (ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-join(C)).(CP1,CP2) = ConceptStr(#O,A#) & O = ( AttributeDerivation(C
)).(( ObjectDerivation(C)). ((the Extent of CP1) \/ (the Extent of CP2))) & A =
(the Intent of CP1) /\ (the Intent of CP2) )& ex O9 being Subset of the carrier
  of C, A9 being Subset of the carrier' of C st (B-meet(C)).(CP1,CP9) =
ConceptStr (#O9,A9#) & O9 = (the Extent of CP1) /\ (the Extent of CP9) & A9 = (
  ObjectDerivation(C)).(( AttributeDerivation(C)). ((the Intent of CP1) \/ (the
  Intent of CP9))) by Def17,Def18;
  (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/
  ((the Intent of CP1) /\ (the Intent of CP2)))) = (ObjectDerivation(C)). (((
AttributeDerivation(C)).(the Intent of CP1)) /\ ((AttributeDerivation(C)).((the
  Intent of CP1) /\ (the Intent of CP2)))) by Th16;
  then
A3: (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP1) \/
  ((the Intent of CP1) /\ (the Intent of CP2)))) = (ObjectDerivation(C)).((
  AttributeDerivation(C)).(the Intent of CP1)) by A1,Th4,XBOOLE_1:28
    .= (ObjectDerivation(C)).(the Extent of CP1) by Def9
    .= the Intent of CP1 by Def9;
  (the Extent of CP1) /\ ((AttributeDerivation(C)).((ObjectDerivation(C)).
  ((the Extent of CP1) \/ (the Extent of CP2)))) = (the Extent of CP1) /\ ((
  AttributeDerivation(C)). (((ObjectDerivation(C)).(the Extent of CP1)) /\ ((
  ObjectDerivation(C)).(the Extent of CP2)))) by Th15
    .= (the Extent of CP1) /\ ((AttributeDerivation(C)). ((the Intent of CP1
  ) /\ ((ObjectDerivation(C)).(the Extent of CP2)))) by Def9
    .= (the Extent of CP1) /\ ((AttributeDerivation(C)). ((the Intent of CP1
  ) /\ (the Intent of CP2))) by Def9
    .= ((AttributeDerivation(C)).(the Intent of CP1)) /\ ((
AttributeDerivation(C)). ((the Intent of CP1) /\ (the Intent of CP2))) by Def9
    .= (AttributeDerivation(C)).(the Intent of CP1) by A1,Th4,XBOOLE_1:28
    .= the Extent of CP1 by Def9;
  hence thesis by A2,A3;
end;

theorem
  for C being FormalContext for CP being strict FormalConcept of C holds
  (B-meet(C)).(CP,Concept-with-all-Objects(C)) = CP
proof
  let C be FormalContext;
  let CP be strict FormalConcept of C;
  consider O being Subset of the carrier of C, A being Subset of the carrier'
  of C such that
A1: (B-meet(C)).(CP,Concept-with-all-Objects(C)) = ConceptStr(#O,A#) and
A2: O = (the Extent of CP) /\ (the Extent of Concept-with-all-Objects(C) ) and
A3: A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of
  CP) \/ (the Intent of Concept-with-all-Objects(C)))) by Def17;
A4: O = (the Extent of CP) /\ the carrier of C by A2,Th23
    .= the Extent of CP by XBOOLE_1:28;
  the carrier of C c= the carrier of C;
  then reconsider O9 = the carrier of C as Subset of the carrier of C;
A5: (ObjectDerivation(C)).(the Extent of CP) \/ (ObjectDerivation(C)).O9 = (
  ObjectDerivation(C)).(the Extent of CP) by Th3,XBOOLE_1:12;
  A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP)
  \/ (ObjectDerivation(C)).(the Extent of Concept-with-all-Objects(C)))) by A3
,Def9
    .= (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP)
  \/ (ObjectDerivation(C)). the carrier of C)) by Th23
    .= (ObjectDerivation(C)).((AttributeDerivation(C)). ((ObjectDerivation(C
  )).(the Extent of CP))) by A5,Def9
    .= (ObjectDerivation(C)).(the Extent of CP) by Th7
    .= the Intent of CP by Def9;
  hence thesis by A1,A4;
end;

theorem Th39:
  for C being FormalContext for CP being strict FormalConcept of C
holds (B-join(C)).(CP,Concept-with-all-Objects(C)) = Concept-with-all-Objects(C
  )
proof
  let C be FormalContext;
  let CP be strict FormalConcept of C;
  consider O being Subset of the carrier of C, A being Subset of the carrier'
  of C such that
A1: (B-join(C)).(CP,Concept-with-all-Objects(C)) = ConceptStr(#O,A#) and
A2: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of
  CP) \/ (the Extent of Concept-with-all-Objects(C)))) and
A3: A = (the Intent of CP) /\ (the Intent of Concept-with-all-Objects(C)
  ) by Def18;
A4: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP)
  \/ the carrier of C)) by A2,Th23
    .= (AttributeDerivation(C)).((ObjectDerivation(C)). the carrier of C) by
XBOOLE_1:12
    .= (AttributeDerivation(C)).((ObjectDerivation(C)). (the Extent of
  Concept-with-all-Objects(C))) by Th23
    .= (AttributeDerivation(C)). (the Intent of Concept-with-all-Objects(C))
  by Def9
    .= the Extent of Concept-with-all-Objects(C) by Def9;
  A = ((ObjectDerivation(C)).(the Extent of CP)) /\ (the Intent of
  Concept-with-all-Objects(C)) by A3,Def9
    .= ((ObjectDerivation(C)).(the Extent of CP)) /\ ((ObjectDerivation(C)).
  (the Extent of Concept-with-all-Objects(C))) by Def9
    .= (ObjectDerivation(C)). ((the Extent of CP) \/ (the Extent of
  Concept-with-all-Objects(C))) by Th15
    .= (ObjectDerivation(C)). ((the Extent of CP) \/ the carrier of C) by Th23
    .= (ObjectDerivation(C)). the carrier of C by XBOOLE_1:12
    .= (ObjectDerivation(C)).(the Extent of Concept-with-all-Objects(C)) by
Th23
    .= the Intent of Concept-with-all-Objects(C) by Def9;
  hence thesis by A1,A4;
end;

theorem
  for C being FormalContext for CP being strict FormalConcept of C holds
  (B-join(C)).(CP,Concept-with-all-Attributes(C)) = CP
proof
  let C be FormalContext;
  let CP be strict FormalConcept of C;
  consider O being Subset of the carrier of C, A being Subset of the carrier'
  of C such that
A1: (B-join(C)).(CP,Concept-with-all-Attributes(C)) = ConceptStr(#O,A#) and
A2: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of
  CP) \/ (the Extent of Concept-with-all-Attributes(C)))) and
A3: A = (the Intent of CP) /\ (the Intent of Concept-with-all-Attributes
  (C)) by Def18;
A4: A = (the Intent of CP) /\ the carrier' of C by A3,Th23
    .= the Intent of CP by XBOOLE_1:28;
  the carrier' of C c= the carrier' of C;
  then reconsider A9 = the carrier' of C as Subset of the carrier' of C;
A5: (AttributeDerivation(C)).(the Intent of CP) \/ (AttributeDerivation(C) )
  .A9 = (AttributeDerivation(C)).(the Intent of CP) by Th4,XBOOLE_1:12;
  O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP)
\/ (AttributeDerivation(C)).(the Intent of Concept-with-all-Attributes(C))))
by A2,Def9
    .= (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP)
  \/ (AttributeDerivation(C)). the carrier' of C)) by Th23
    .= (AttributeDerivation(C)).((ObjectDerivation(C)). ((
  AttributeDerivation(C)).(the Intent of CP))) by A5,Def9
    .= (AttributeDerivation(C)).(the Intent of CP) by Th8
    .= the Extent of CP by Def9;
  hence thesis by A1,A4;
end;

theorem
  for C being FormalContext for CP being strict FormalConcept of C holds
(B-meet(C)).(CP,Concept-with-all-Attributes(C)) = Concept-with-all-Attributes(C
  )
proof
  let C be FormalContext;
  let CP be strict FormalConcept of C;
  consider O being Subset of the carrier of C, A being Subset of the carrier'
  of C such that
A1: (B-meet(C)).(CP,Concept-with-all-Attributes(C)) = ConceptStr(#O,A#) and
A2: O = (the Extent of CP) /\ (the Extent of Concept-with-all-Attributes
  (C)) and
A3: A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of
  CP) \/ (the Intent of Concept-with-all-Attributes(C)))) by Def17;
A4: A = (ObjectDerivation(C)).((AttributeDerivation(C)). ((the Intent of CP)
  \/ the carrier' of C)) by A3,Th23
    .= (ObjectDerivation(C)).((AttributeDerivation(C)). the carrier' of C)
  by XBOOLE_1:12
    .= (ObjectDerivation(C)).((AttributeDerivation(C)). (the Intent of
  Concept-with-all-Attributes(C))) by Th23
    .= (ObjectDerivation(C)).(the Extent of Concept-with-all-Attributes(C))
  by Def9
    .= the Intent of Concept-with-all-Attributes(C) by Def9;
  O = ((AttributeDerivation(C)).(the Intent of CP)) /\ (the Extent of
  Concept-with-all-Attributes(C)) by A2,Def9
    .= ((AttributeDerivation(C)).(the Intent of CP)) /\ ((
  AttributeDerivation(C)). (the Intent of Concept-with-all-Attributes(C))) by
Def9
    .= (AttributeDerivation(C)). ((the Intent of CP) \/ (the Intent of
  Concept-with-all-Attributes(C))) by Th16
    .= (AttributeDerivation(C)). ((the Intent of CP) \/ the carrier' of C)
  by Th23
    .= (AttributeDerivation(C)). the carrier' of C by XBOOLE_1:12
    .= (AttributeDerivation(C)).(the Intent of Concept-with-all-Attributes(C
  )) by Th23
    .= the Extent of Concept-with-all-Attributes(C) by Def9;
  hence thesis by A1,A4;
end;

definition
  let C be FormalContext;
  func ConceptLattice(C) -> strict non empty LattStr equals
  LattStr(#B-carrier
    (C),B-join(C),B-meet(C)#);
  coherence;
end;

theorem Th42:
  for C being FormalContext holds ConceptLattice(C) is Lattice
proof
  let C be FormalContext;
  set L = LattStr(#B-carrier(C),B-join(C),B-meet(C)#);
  reconsider L as strict non empty LattStr;
A1: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b) "\/"c
  proof
    let a,b,c be Element of L;
    reconsider b,c as Element of B-carrier(C);
    reconsider d = (B-join(C)).(b,c) as Element of L;
    reconsider b,c as Element of L;
    reconsider a,b as Element of B-carrier(C);
    reconsider e = (B-join(C)).(a,b) as Element of L;
    reconsider a,b as Element of L;
A2: a"\/"(b"\/"c) = a"\/"d by LATTICES:def 1
      .= (B-join(C)).(a,(B-join(C)).(b,c)) by LATTICES:def 1;
A3: (a"\/"b)"\/"c = e"\/"c by LATTICES:def 1
      .= (B-join(C)).((B-join(C)).(a,b),c) by LATTICES:def 1;
    reconsider a,b,c as strict FormalConcept of C by Th31;
    (B-join(C)).(a,(B-join(C)).(b,c)) = (B-join(C)).((B-join(C)).(a,b),c)
    by Th35;
    hence thesis by A2,A3;
  end;
A4: for a,b being Element of L holds (a"/\"b)"\/"b = b
  proof
    let a,b be Element of L;
    reconsider a,b as Element of B-carrier(C);
    reconsider d = (B-meet(C)).(a,b) as Element of L;
    reconsider a,b as Element of L;
A5: (a"/\"b)"\/"b = d"\/"b by LATTICES:def 2
      .= (B-join(C)).((B-meet(C)).(a,b),b) by LATTICES:def 1;
    reconsider a,b as strict FormalConcept of C by Th31;
    (B-join(C)).((B-meet(C)).(a,b),b) = b by Th36;
    hence thesis by A5;
  end;
A6: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\" b)"/\"c
  proof
    let a,b,c be Element of L;
    reconsider b,c as Element of B-carrier(C);
    reconsider d = (B-meet(C)).(b,c) as Element of L;
    reconsider b,c as Element of L;
A7: a"/\"(b"/\"c) = a"/\"d by LATTICES:def 2
      .= (B-meet(C)).(a,(B-meet(C)).(b,c)) by LATTICES:def 2;
    reconsider a,b as Element of B-carrier(C);
    reconsider e = (B-meet(C)).(a,b) as Element of L;
    reconsider a,b as Element of L;
A8: (a"/\"b)"/\"c = e"/\"c by LATTICES:def 2
      .= (B-meet(C)).((B-meet(C)).(a,b),c) by LATTICES:def 2;
    reconsider a,b,c as strict FormalConcept of C by Th31;
    (B-meet(C)).(a,(B-meet(C)).(b,c)) = (B-meet(C)).((B-meet(C)).(a,b),c)
    by Th34;
    hence thesis by A7,A8;
  end;
A9: for a,b being Element of L holds a"/\"b = b"/\"a
  proof
    let a,b be Element of L;
A10: b"/\"a = (B-meet(C)).(b,a) by LATTICES:def 2;
    reconsider a,b as strict FormalConcept of C by Th31;
    (B-meet(C)).(a,b) = (B-meet(C)).(b,a) by Th32;
    hence thesis by A10,LATTICES:def 2;
  end;
A11: for a,b being Element of L holds a"/\"(a"\/"b)=a
  proof
    let a,b be Element of L;
    reconsider a,b as Element of B-carrier(C);
    reconsider d = (B-join(C)).(a,b) as Element of L;
    reconsider a,b as Element of L;
A12: a"/\"(a"\/"b) = a"/\"d by LATTICES:def 1
      .= (B-meet(C)).(a,(B-join(C)).(a,b)) by LATTICES:def 2;
    reconsider a,b as strict FormalConcept of C by Th31;
    (B-meet(C)).(a,(B-join(C)).(a,b)) = a by Th37;
    hence thesis by A12;
  end;
  for a,b being Element of L holds a"\/"b = b"\/"a
  proof
    let a,b be Element of L;
A13: b"\/"a = (B-join(C)).(b,a) by LATTICES:def 1;
    reconsider a,b as strict FormalConcept of C by Th31;
    (B-join(C)).(a,b) = (B-join(C)).(b,a) by Th33;
    hence thesis by A13,LATTICES:def 1;
  end;
  then L is join-commutative join-associative meet-absorbing meet-commutative
  meet-associative join-absorbing by A1,A4,A9,A6,A11,LATTICES:def 4,def 5,def 6
,def 7,def 8,def 9;
  hence thesis;
end;

registration
  let C be FormalContext;
  cluster ConceptLattice(C) -> strict non empty Lattice-like;
  coherence by Th42;
end;

definition
  let C be FormalContext;
  let S be non empty Subset of ConceptLattice(C);
  redefine mode Element of S -> FormalConcept of C;
  coherence
  proof
    let s be Element of S;
    s is Element of B-carrier(C);
    hence thesis;
  end;
end;

definition
  let C be FormalContext;
  let CP be Element of ConceptLattice(C);
  func CP@ -> strict FormalConcept of C equals
  CP;
  coherence by Th31;
end;

theorem Th43:
  for C being FormalContext for CP1,CP2 being Element of
  ConceptLattice(C) holds CP1 [= CP2 iff CP1@ is-SubConcept-of CP2@
proof
  let C be FormalContext;
  let CP1,CP2 be Element of ConceptLattice(C);
  set CL = ConceptLattice(C);
A1: now
    assume
A2: CP1@ is-SubConcept-of CP2@;
    then the Intent of CP2@ c= the Intent of CP1@ by Th28;
    then
A3: (the Intent of CP1@) /\ (the Intent of CP2@) = the Intent of CP2@ by
XBOOLE_1:28;
    consider O being Subset of the carrier of C, A being Subset of the
    carrier' of C such that
A4: (B-join(C)).(CP1@,CP2@) = ConceptStr(#O,A#) and
A5: O = (AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent
    of CP1@) \/ (the Extent of CP2@))) and
A6: A = (the Intent of CP1@) /\ (the Intent of CP2@) by Def18;
    the Extent of CP1@ c= the Extent of CP2@ by A2;
    then (the Extent of CP1@) \/ (the Extent of CP2@) = the Extent of CP2@ by
XBOOLE_1:12;
    then O = (AttributeDerivation(C)).(the Intent of CP2@) by A5,Def9
      .= the Extent of CP2@ by Def9;
    then CP1 "\/" CP2 = CP2 by A3,A4,A6,LATTICES:def 1;
    hence CP1 [= CP2 by LATTICES:def 3;
  end;
  now
    assume CP1 [= CP2;
    then CP1 "\/" CP2 = CP2 by LATTICES:def 3;
    then
A7: (the L_join of CL).(CP1,CP2) = CP2 by LATTICES:def 1;
    ex O being Subset of the carrier of C, A being Subset of the carrier'
of C st (B-join(C)).(CP1@,CP2@) = ConceptStr(#O,A#) & O = ( AttributeDerivation
(C)).((ObjectDerivation(C)). ((the Extent of CP1@) \/ (the Extent of CP2@))) &
    A = (the Intent of CP1@) /\ (the Intent of CP2@) by Def18;
    then
    for x being object holds x in the Intent of CP2@ implies x in the Intent
    of CP1@ by A7,XBOOLE_0:def 4;
    then the Intent of CP2@ c= the Intent of CP1@;
    hence CP1@ is-SubConcept-of CP2@ by Th28;
  end;
  hence thesis by A1;
end;

theorem Th44:
  for C being FormalContext holds ConceptLattice(C) is complete Lattice
proof
  let C be FormalContext;
  for X being Subset of ConceptLattice(C) ex a being Element of
ConceptLattice(C) st a is_less_than X & for b being Element of ConceptLattice(C
  ) st b is_less_than X holds b [= a
  proof
    let X be Subset of ConceptLattice(C);
    per cases;
    suppose
A1:   X = {};
A2:   for b being Element of ConceptLattice(C) st b is_less_than X holds b
      [= Top ConceptLattice(C)
      proof
        let b be Element of ConceptLattice(C);
        assume b is_less_than X;
        ex c being Element of ConceptLattice(C) st for a being Element of
        ConceptLattice(C) holds c"\/"a = c & a"\/"c = c
        proof
          reconsider CO = Concept-with-all-Objects(C) as Element of
          ConceptLattice(C) by Th31;
          for CP being Element of ConceptLattice(C) holds CO "\/" CP = CO
          & CP "\/" CO = CO
          proof
            let CP be Element of ConceptLattice(C);
            reconsider CP as strict FormalConcept of C by Th31;
            reconsider CO as strict FormalConcept of C;
            (B-join(C)).(CO,CP) = (B-join(C)).(CP,CO) by Th33
              .= CO by Th39;
            hence thesis by LATTICES:def 1;
          end;
          hence thesis;
        end;
        then ConceptLattice(C) is upper-bounded by LATTICES:def 14;
        then Top ConceptLattice(C) "\/" b = Top ConceptLattice(C);
        hence thesis by LATTICES:def 3;
      end;
      for q being Element of ConceptLattice(C) st q in X holds Top
      ConceptLattice(C) [= q by A1;
      then Top ConceptLattice(C) is_less_than X by LATTICE3:def 16;
      hence thesis by A2;
    end;
    suppose
      X <> {};
      then reconsider X as non empty Subset of ConceptLattice(C);
      set ExX = { the Extent of x where x is Element of B-carrier(C) : x in X
      };
A3:   for x being Element of X holds the Extent of x in ExX
      proof
        let x be Element of X;
        x in X;
        then reconsider x as Element of B-carrier(C);
        the Extent of x in ExX;
        hence thesis;
      end;
      then reconsider ExX as non empty set;
      set E1 = meet ExX;
A4:   for o being Object of C holds o in E1 iff for x being Element of X
      holds o in the Extent of x
      proof
        let o be Object of C;
A5:     (for x being Element of X holds o in the Extent of x) implies o in E1
        proof
          assume
A6:       for x being Element of X holds o in the Extent of x;
          for Y being set holds Y in ExX implies o in Y
          proof
            let Y be set;
            assume Y in ExX;
            then
            ex Y9 being Element of B-carrier(C) st Y = the Extent of Y9 &
            Y9 in X;
            hence thesis by A6;
          end;
          hence thesis by SETFAM_1:def 1;
        end;
        o in E1 implies for x being Element of X holds o in the Extent of x
        proof
          assume
A7:       o in E1;
          let x be Element of X;
          the Extent of x in ExX by A3;
          hence thesis by A7,SETFAM_1:def 1;
        end;
        hence thesis by A5;
      end;
      E1 c= the carrier of C
      proof
        set Y = the Element of ExX;
        let x be object;
        Y in ExX;
        then consider Y9 being Element of B-carrier(C) such that
A8:     Y = the Extent of Y9 and
        Y9 in X;
        assume x in E1;
        then x in the Extent of Y9 by A8,SETFAM_1:def 1;
        hence thesis;
      end;
      then consider O being Subset of the carrier of C such that
A9:   for o being Object of C holds o in O iff for x being Element of
      X holds o in the Extent of x by A4;
      set InX = { the Intent of x where x is Element of B-carrier(C) : x in X
      };
      set In = union InX;
A10:  for a being Attribute of C holds a in In iff ex x being Element of
      X st a in the Intent of x
      proof
        let a be Attribute of C;
A11:    (ex x being Element of X st a in the Intent of x) implies a in In
        proof
          assume
A12:      ex x being Element of X st a in the Intent of x;
          ex Y being set st a in Y & Y in InX
          proof
            consider x being Element of X such that
A13:        a in the Intent of x by A12;
            x in X;
            then the Intent of x in InX;
            hence thesis by A13;
          end;
          hence thesis by TARSKI:def 4;
        end;
        a in In implies ex x being Element of X st a in the Intent of x
        proof
          assume a in In;
          then consider Y being set such that
A14:      a in Y and
A15:      Y in InX by TARSKI:def 4;
          ex Y9 being Element of B-carrier(C) st Y = the Intent of Y9 & Y9
          in X by A15;
          hence thesis by A14;
        end;
        hence thesis by A11;
      end;
      In c= the carrier' of C
      proof
        let x be object;
        assume x in In;
        then consider Y being set such that
A16:    x in Y and
A17:    Y in InX by TARSKI:def 4;
        ex Y9 being Element of B-carrier(C) st Y = the Intent of Y9 & Y9
        in X by A17;
        hence thesis by A16;
      end;
      then consider A9 being Subset of the carrier' of C such that
A18:  for a being Attribute of C holds a in A9 iff ex x being Element
      of X st a in the Intent of x by A10;
A19:  for o being Object of C holds o in O iff for x being Element of X
      holds o in (AttributeDerivation(C)).(the Intent of x)
      proof
        let o be Object of C;
A20:    (for x being Element of X holds o in (AttributeDerivation(C)).(
        the Intent of x)) implies o in O
        proof
          assume
A21:      for x being Element of X holds o in (AttributeDerivation(C)
          ).(the Intent of x);
          for x being Element of X holds o in the Extent of x
          proof
            let x be Element of X;
            o in (AttributeDerivation(C)).(the Intent of x) by A21;
            hence thesis by Def9;
          end;
          hence thesis by A9;
        end;
        o in O implies for x being Element of X holds o in (
        AttributeDerivation(C)).(the Intent of x)
        proof
          assume
A22:      o in O;
          for x being Element of X holds o in (AttributeDerivation(C)).(
          the Intent of x)
          proof
            let x be Element of X;
            o in the Extent of x by A9,A22;
            hence thesis by Def9;
          end;
          hence thesis;
        end;
        hence thesis by A20;
      end;
A23:  for x being object holds x in (AttributeDerivation(C)).A9 implies x in O
      proof
        let x be object;
        assume x in (AttributeDerivation(C)).A9;
        then x in {o where o is Object of C : for a being Attribute of C st a
        in A9 holds o is-connected-with a} by Def3;
        then consider x9 being Object of C such that
A24:    x9 = x and
A25:    for a being Attribute of C st a in A9 holds x9 is-connected-with a;
        for x being Element of X holds x9 in (AttributeDerivation(C)).(
        the Intent of x)
        proof
          let x be Element of X;
          for a being Attribute of C st a in (the Intent of x) holds x9
          is-connected-with a by A18,A25;
          then x9 in {o where o is Object of C :
          for a being Attribute of C st
           a in (the Intent of x) holds o is-connected-with a};
          hence thesis by Def3;
        end;
        hence thesis by A19,A24;
      end;
      consider A being Subset of the carrier' of C such that
A26:  A = (ObjectDerivation(C)).((AttributeDerivation(C)).A9);
      set p = ConceptStr(#O,A#);
      for x being object
          holds x in O implies x in (AttributeDerivation(C)). A9
      proof
        let x9 be object;
        assume
A27:    x9 in O;
        then reconsider x9 as Object of C;
        for a being Attribute of C st a in A9 holds x9 is-connected-with a
        proof
          let a be Attribute of C;
          assume a in A9;
          then consider x being Element of X such that
A28:      a in the Intent of x by A18;
          x9 in (AttributeDerivation(C)).(the Intent of x) by A19,A27;
          then
          x9 in {o where o is Object of C : for a being Attribute of C st
          a in the Intent of x holds o is-connected-with a} by Def3;
          then
          ex y being Object of C st y = x9 & for a being Attribute of C st
          a in the Intent of x holds y is-connected-with a;
          hence thesis by A28;
        end;
        then
        x9 in {o where o is Object of C : for a being Attribute of C st a
        in A9 holds o is-connected-with a};
        hence thesis by Def3;
      end;
      then O = (AttributeDerivation(C)).A9 by A23,TARSKI:2;
      then p is FormalConcept of C by A26,Th21;
      then reconsider p as Element of ConceptLattice(C) by Th31;
A29:  for b being Element of ConceptLattice(C) st b is_less_than X holds b [= p
      proof
        let b be Element of ConceptLattice(C);
        assume
A30:    b is_less_than X;
        the Extent of b@ c= the Extent of p@
        proof
          let x9 be object;
          assume
A31:      x9 in the Extent of b@;
          then reconsider x9 as Object of C;
          for x being Element of X holds x9 in the Extent of x
          proof
            let x be Element of X;
            x in X;
            then reconsider x as Element of ConceptLattice(C);
            b [= x by A30,LATTICE3:def 16;
            then b@ is-SubConcept-of x@ by Th43;
            then the Extent of b@ c= the Extent of x@;
            hence thesis by A31;
          end;
          hence thesis by A9;
        end;
        then b@ is-SubConcept-of p@;
        hence thesis by Th43;
      end;
      for q being Element of ConceptLattice(C) st q in X holds p [= q
      proof
        let q be Element of ConceptLattice(C);
        assume
A32:    q in X;
        the Extent of p@ c= the Extent of q@
        by A9,A32;
        then p@ is-SubConcept-of q@;
        hence thesis by Th43;
      end;
      then p is_less_than X by LATTICE3:def 16;
      hence thesis by A29;
    end;
  end;
  hence thesis by VECTSP_8:def 6;
end;

registration
  let C be FormalContext;
  cluster ConceptLattice(C) -> complete;
  coherence by Th44;
end;