:: CONLAT_1 semantic presentation

begin

definition
let C be 2-sorted ;
attrC is quasi-empty  means :Def1: :: CONLAT_1:def 1
( the carrier of C is empty or the carrier' of C is empty );
end;

:: deftheorem Def1 defines quasi-empty CONLAT_1:def_1_:_
 for C being 2-sorted holds
( C is quasi-empty iff ( the carrier of C is empty or the carrier' of C is empty ) );

registration
cluster non empty strict non void for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void )
proof
 ( not 2-sorted(# {{}},{{}} #) is empty & not 2-sorted(# {{}},{{}} #) is void ) ;
hence  ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void ) ; ::_thesis: verum
end;
cluster strict non quasi-empty for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & not b1 is quasi-empty )
proof
 not 2-sorted(# {{}},{{}} #) is quasi-empty by Def1;
hence  ex b1 being 2-sorted st
( b1 is strict & not b1 is quasi-empty ) ; ::_thesis: verum
end;
end;

registration
cluster empty strict void quasi-empty for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void & b1 is quasi-empty )
proof
 ( 2-sorted(# {},{} #) is empty & 2-sorted(# {},{} #) is void & 2-sorted(# {},{} #) is quasi-empty ) by Def1;
hence  ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void & b1 is quasi-empty ) ; ::_thesis: verum
end;
end;

definition
attrc1 is strict ;
struct ContextStr  ->  2-sorted ;
aggrContextStr(# carrier, carrier', Information #) ->  ContextStr ;
sel Information c1 ->  Relation of the carrier of c1, the carrier' of c1;
end;

registration
cluster non empty strict for ContextStr ;
existence
 ex b1 being ContextStr st
( b1 is strict & not b1 is empty )
proof
set I = the Relation of {{}},{{}};
 not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is empty ;
hence  ex b1 being ContextStr st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
cluster non quasi-empty strict for ContextStr ;
existence
 ex b1 being ContextStr st
( b1 is strict & not b1 is quasi-empty )
proof
set I = the Relation of {{}},{{}};
 not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is quasi-empty by Def1;
hence  ex b1 being ContextStr st
( b1 is strict & not b1 is quasi-empty ) ; ::_thesis: verum
end;
end;

definition
mode FormalContext is non quasi-empty 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 quasi-empty 2-sorted ;
cluster the carrier' of C ->  non empty ;
coherence
 not the carrier' of C is empty by Def1;
cluster the carrier of C ->  non empty ;
coherence
 not the carrier of C is empty by Def1;
end;

registration
let C be non quasi-empty 2-sorted ;
cluster non empty for Element of bool the carrier of C;
existence
 not for b1 being Subset of the carrier of C holds b1 is empty
proof
take  the carrier of C ; ::_thesis: ( the carrier of C is Subset of the carrier of C & not the carrier of C is empty )
 the carrier of C c= the carrier of C ;
hence  ( the carrier of C is Subset of the carrier of C & not the carrier of C is empty ) ; ::_thesis: verum
end;
cluster non empty for Element of bool the carrier' of C;
existence
 not for b1 being Subset of the carrier' of C holds b1 is empty
proof
take  the carrier' of C ; ::_thesis: ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty )
 the carrier' of C c= the carrier' of C ;
hence  ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty ) ; ::_thesis: verum
end;
end;

definition
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
predo is-connected-with a means :Def2: :: CONLAT_1:def 2
[o,a] in the Information of C;
end;

:: deftheorem Def2 defines is-connected-with CONLAT_1:def_2_:_
 for C being FormalContext
for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff [o,a] in the Information of C );

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;

begin

definition
let C be FormalContext;
func ObjectDerivation C ->  Function of (bool the carrier of C),(bool the carrier' of C) means :Def3: :: CONLAT_1:def 3
 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
 ex b1 being Function of (bool the carrier of C),(bool the carrier' of C) st
for O being Subset of the carrier of C holds b1 . 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
set 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  }  ] where O is Subset of the carrier of C : verum  }  ;
 for u being set st u in  {  [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 : verum  }  holds
ex v, w being set st u = [v,w]
proof
let u be set ; ::_thesis: ( u in  {  [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 : verum  }  implies ex v, w being set st u = [v,w] )
assume  u in  {  [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 : verum  }  ; ::_thesis: ex v, w being set st u = [v,w]
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  ex v, w being set st u = [v,w] ; ::_thesis: verum
end;
then reconsider 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  }  ] where O is Subset of the carrier of C : verum  }  as Relation by RELAT_1:def_1;
 for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds
v1 = v2
proof
let u, v1, v2 be set ; ::_thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume that
A1: [u,v1] in f and
A2: [u,v2] in f ; ::_thesis: v1 = v2
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  v1 = v2 by A4, A6; ::_thesis: verum
end;
then reconsider f = f as Function by FUNCT_1:def_1;
A7: for x being set st x in dom f holds
x in bool the carrier of C
proof
let x be set ; ::_thesis: ( x in dom f implies x in bool the carrier of C )
assume  x in dom f ; ::_thesis: x in bool the carrier of C
then consider y being set  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  x in bool the carrier of C ; ::_thesis: verum
end;
 for x being set st x in bool the carrier of C holds
x in dom f
proof
let x be set ; ::_thesis: ( x in bool the carrier of C implies x in dom f )
assume  x in bool the carrier of C ; ::_thesis: x in dom f
then reconsider x = 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  x in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A10: dom f = bool the carrier of C by A7, TARSKI:1;
 rng f c= bool the carrier' of C
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier' of C )
assume  y in rng f ; ::_thesis: y in bool the carrier' of C
then consider x being set  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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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  }  or u in the carrier' of C )
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  }  ; ::_thesis: u in the carrier' of C
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  u in the carrier' of C ; ::_thesis: verum
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  y in bool the carrier' of C by A13; ::_thesis: verum
end;
then reconsider f = 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 ; ::_thesis: 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  }
 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; ::_thesis: 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  }
consider y being set  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  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  }  by A10, A14, A16, FUNCT_1:def_2; ::_thesis: verum
end;
hence  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  }  ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (bool the carrier of C),(bool the carrier' of C) st ( for O being Subset of the carrier of C holds b1 . O =  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  ) & ( for O being Subset of the carrier of C holds b2 . O =  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  ) holds
b1 = b2
proof
let F1, F2 be Function of (bool the carrier of C),(bool the carrier' of C); ::_thesis: ( ( 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  }  ) & ( 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  }  ) implies F1 = F2 )
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  }  ; ::_thesis: ( ex O being Subset of the carrier of C st not 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  }  or F1 = F2 )
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  }  ; ::_thesis: F1 = F2
A19: for O being set st O in bool the carrier of C holds
F1 . O = F2 . O
proof
let O be set ; ::_thesis: ( O in bool the carrier of C implies F1 . O = F2 . O )
assume  O in bool the carrier of C ; ::_thesis: F1 . O = F2 . O
then reconsider O = 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  F1 . O = F2 . O ; ::_thesis: verum
end;
 ( dom F1 = bool the carrier of C & dom F2 = bool the carrier of C ) by FUNCT_2:def_1;
hence  F1 = F2 by A19, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines ObjectDerivation CONLAT_1:def_3_:_
 for C being FormalContext
for b2 being Function of (bool the carrier of C),(bool the carrier' of C) holds
( b2 = ObjectDerivation C iff for O being Subset of the carrier of C holds b2 . O =  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  );

definition
let C be FormalContext;
func AttributeDerivation C ->  Function of (bool the carrier' of C),(bool the carrier of C) means :Def4: :: CONLAT_1:def 4
 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
 ex b1 being Function of (bool the carrier' of C),(bool the carrier of C) st
for A being Subset of the carrier' of C holds b1 . 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
set 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  }  ] where A is Subset of the carrier' of C : verum  }  ;
 for u being set st u in  {  [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 : verum  }  holds
ex v, w being set st u = [v,w]
proof
let u be set ; ::_thesis: ( u in  {  [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 : verum  }  implies ex v, w being set st u = [v,w] )
assume  u in  {  [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 : verum  }  ; ::_thesis: ex v, w being set st u = [v,w]
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  ex v, w being set st u = [v,w] ; ::_thesis: verum
end;
then reconsider 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  }  ] where A is Subset of the carrier' of C : verum  }  as Relation by RELAT_1:def_1;
 for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds
v1 = v2
proof
let u, v1, v2 be set ; ::_thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume that
A1: [u,v1] in f and
A2: [u,v2] in f ; ::_thesis: v1 = v2
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  v1 = v2 by A4, A6; ::_thesis: verum
end;
then reconsider f = f as Function by FUNCT_1:def_1;
A7: for x being set st x in dom f holds
x in bool the carrier' of C
proof
let x be set ; ::_thesis: ( x in dom f implies x in bool the carrier' of C )
assume  x in dom f ; ::_thesis: x in bool the carrier' of C
then consider y being set  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  x in bool the carrier' of C ; ::_thesis: verum
end;
 for x being set st x in bool the carrier' of C holds
x in dom f
proof
let x be set ; ::_thesis: ( x in bool the carrier' of C implies x in dom f )
assume  x in bool the carrier' of C ; ::_thesis: x in dom f
then reconsider x = 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  x in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A10: dom f = bool the carrier' of C by A7, TARSKI:1;
 rng f c= bool the carrier of C
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier of C )
assume  y in rng f ; ::_thesis: y in bool the carrier of C
then consider x being set  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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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  }  or u in the carrier of C )
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  }  ; ::_thesis: u in the carrier of C
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  u in the carrier of C ; ::_thesis: verum
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  y in bool the carrier of C by A13; ::_thesis: verum
end;
then reconsider f = 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 ; ::_thesis: 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  }
 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; ::_thesis: 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  }
consider y being set  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  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  }  by A10, A14, A16, FUNCT_1:def_2; ::_thesis: verum
end;
hence  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  }  ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (bool the carrier' of C),(bool the carrier of C) st ( for A being Subset of the carrier' of C holds b1 . A =  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  ) & ( for A being Subset of the carrier' of C holds b2 . A =  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  ) holds
b1 = b2
proof
let F1, F2 be Function of (bool the carrier' of C),(bool the carrier of C); ::_thesis: ( ( 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  }  ) & ( 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  }  ) implies F1 = F2 )
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  }  ; ::_thesis: ( ex A being Subset of the carrier' of C st not 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  }  or F1 = F2 )
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  }  ; ::_thesis: F1 = F2
A19: for A being set st A in bool the carrier' of C holds
F1 . A = F2 . A
proof
let A be set ; ::_thesis: ( A in bool the carrier' of C implies F1 . A = F2 . A )
assume  A in bool the carrier' of C ; ::_thesis: F1 . A = F2 . A
then reconsider A = 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  F1 . A = F2 . A ; ::_thesis: verum
end;
 ( dom F1 = bool the carrier' of C & dom F2 = bool the carrier' of C ) by FUNCT_2:def_1;
hence  F1 = F2 by A19, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines AttributeDerivation CONLAT_1:def_4_:_
 for C being FormalContext
for b2 being Function of (bool the carrier' of C),(bool the carrier of C) holds
( b2 = AttributeDerivation C iff for A being Subset of the carrier' of C holds b2 . A =  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  );

theorem :: CONLAT_1:1
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; ::_thesis: for o being Object of C holds (ObjectDerivation C) . {o} =  {  a where a is Attribute of C : o is-connected-with a  }
let o be Object of C; ::_thesis: (ObjectDerivation C) . {o} =  {  a where a is Attribute of C : o is-connected-with a  }
 {o} c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {o} or x in the carrier of C )
assume  x in {o} ; ::_thesis: x in the carrier of C
then  x = o by TARSKI:def_1;
hence  x in the carrier of C ; ::_thesis: verum
end;
then reconsider t = {o} as Subset of the carrier of C ;
A1: for x being set st 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  }  holds
x in  {  a where a is Attribute of C : o is-connected-with a  }
proof
set o9 = the Element of t;
let x be set ; ::_thesis: ( 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  }  )
reconsider o9 = the Element of t 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  }  ; ::_thesis: x in  {  a where a is Attribute of C : o 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 = x as Attribute of C ;
 o9 is-connected-with x by A3;
hence  x in  {  a where a is Attribute of C : o is-connected-with a  }  by A2; ::_thesis: verum
end;
A4: for x being set st x in  {  a where a is Attribute of C : o is-connected-with a  }  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  }
proof
let x be set ; ::_thesis: ( 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  }  )
assume  x in  {  a where a is Attribute of C : o is-connected-with a  }  ; ::_thesis: 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 A5: ex x9 being Attribute of C st
( x9 = x & o is-connected-with x9 ) ;
then reconsider x = 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  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  }  ; ::_thesis: verum
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 Def3;
hence  (ObjectDerivation C) . {o} =  {  a where a is Attribute of C : o is-connected-with a  }  by A1, A4, TARSKI:1; ::_thesis: verum
end;

theorem :: CONLAT_1:2
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; ::_thesis: for a being Attribute of C holds (AttributeDerivation C) . {a} =  {  o where o is Object of C : o is-connected-with a  }
let a be Attribute of C; ::_thesis: (AttributeDerivation C) . {a} =  {  o where o is Object of C : o is-connected-with a  }
 {a} c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} or x in the carrier' of C )
assume  x in {a} ; ::_thesis: x in the carrier' of C
then  x = a by TARSKI:def_1;
hence  x in the carrier' of C ; ::_thesis: verum
end;
then reconsider t = {a} as Subset of the carrier' of C ;
A1: for x being set st 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  }  holds
x in  {  o where o is Object of C : o is-connected-with a  }
proof
set a9 = the Element of t;
let x be set ; ::_thesis: ( 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  }  )
reconsider a9 = the Element of t 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  }  ; ::_thesis: x in  {  o where o is Object of C : o is-connected-with a  }
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 = x as Object of C ;
 x is-connected-with a9 by A3;
hence  x in  {  o where o is Object of C : o is-connected-with a  }  by A2; ::_thesis: verum
end;
A4: for x being set st x in  {  o where o is Object of C : o is-connected-with a  }  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  }
proof
let x be set ; ::_thesis: ( 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  }  )
assume  x in  {  o where o is Object of C : o is-connected-with a  }  ; ::_thesis: 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 A5: ex x9 being Object of C st
( x9 = x & x9 is-connected-with a ) ;
then reconsider x = 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  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  }  ; ::_thesis: verum
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 Def4;
hence  (AttributeDerivation C) . {a} =  {  o where o is Object of C : o is-connected-with a  }  by A1, A4, TARSKI:1; ::_thesis: verum
end;

theorem Th3: :: CONLAT_1:3
for C being FormalContext
for O1, O2 being Subset of the carrier of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
proof
let C be FormalContext; ::_thesis: for O1, O2 being Subset of the carrier of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
let O1, O2 be Subset of the carrier of C; ::_thesis: ( O1 c= O2 implies (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 )
assume A1: O1 c= O2 ; ::_thesis: (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . O2 or x in (ObjectDerivation C) . O1 )
assume  x in (ObjectDerivation C) . O2 ; ::_thesis: x in (ObjectDerivation C) . O1
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 Def3;
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  x in (ObjectDerivation C) . O1 by Def3; ::_thesis: verum
end;

theorem Th4: :: CONLAT_1:4
for C being FormalContext
for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds
(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1
proof
let C be FormalContext; ::_thesis: for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds
(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1
let A1, A2 be Subset of the carrier' of C; ::_thesis: ( A1 c= A2 implies (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1 )
assume A1: A1 c= A2 ; ::_thesis: (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . A2 or x in (AttributeDerivation C) . A1 )
assume  x in (AttributeDerivation C) . A2 ; ::_thesis: x in (AttributeDerivation C) . A1
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 Def4;
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  x in (AttributeDerivation C) . A1 by Def4; ::_thesis: verum
end;

theorem Th5: :: CONLAT_1:5
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; ::_thesis: for O being Subset of the carrier of C holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
let O be Subset of the carrier of C; ::_thesis: O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
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 set st 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  }  holds
x in the carrier' of C
proof
let x be set ; ::_thesis: ( 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  }  implies x in the carrier' of C )
assume  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  }  ; ::_thesis: x in the carrier' of C
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  x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A =  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  as Subset of the carrier' of C by TARSKI:def_3;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O or x in (AttributeDerivation C) . ((ObjectDerivation C) . O) )
assume A1: x in O ; ::_thesis: x in (AttributeDerivation C) . ((ObjectDerivation C) . O)
then reconsider x = 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; ::_thesis: ( a in A implies x is-connected-with a )
assume  a in A ; ::_thesis: x is-connected-with 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  x is-connected-with a by A1; ::_thesis: verum
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 Def4;
then  x in (AttributeDerivation C) . A by A2;
hence  x in (AttributeDerivation C) . ((ObjectDerivation C) . O) by Def3; ::_thesis: verum
end;

theorem Th6: :: CONLAT_1:6
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; ::_thesis: for A being Subset of the carrier' of C holds A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
let A be Subset of the carrier' of C; ::_thesis: A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
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 set st 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  }  holds
x in the carrier of C
proof
let x be set ; ::_thesis: ( 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  }  implies x in the carrier of C )
assume  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  }  ; ::_thesis: x in the carrier of C
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  x in the carrier of C ; ::_thesis: verum
end;
then reconsider O =  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  as Subset of the carrier of C by TARSKI:def_3;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (ObjectDerivation C) . ((AttributeDerivation C) . A) )
assume A1: x in A ; ::_thesis: x in (ObjectDerivation C) . ((AttributeDerivation C) . A)
then reconsider x = 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; ::_thesis: ( o in O implies o is-connected-with x )
assume  o in O ; ::_thesis: o is-connected-with x
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  o is-connected-with x by A1; ::_thesis: verum
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 Def3;
then  x in (ObjectDerivation C) . O by A2;
hence  x in (ObjectDerivation C) . ((AttributeDerivation C) . A) by Def4; ::_thesis: verum
end;

theorem Th7: :: CONLAT_1:7
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; ::_thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
let O be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
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 where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with 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 where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  ;
A1: for x being set st x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
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  }
proof
let x be set ; ::_thesis: ( x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  implies 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  }  )
assume  x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: 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  }
then A2: ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with x9 ) ) ;
then reconsider x = 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; ::_thesis: ( o in O implies o is-connected-with x )
assume A3: o in O ; ::_thesis: o is-connected-with x
now__::_thesis:_(_(_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in_O_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_o_is-connected-with_x_)_or_(_not_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in_O_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_o_is-connected-with_x_)_)
percases ( o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  or not o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  ) ;
case o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: o is-connected-with x
hence  o is-connected-with x by A2; ::_thesis: verum
end;
case not o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: o is-connected-with x
then consider a being Attribute of C such that
A4: a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with 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  o is-connected-with x by A3, A5; ::_thesis: verum
end;
end;
end;
hence  o is-connected-with x ; ::_thesis: verum
end;
hence  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  }  ; ::_thesis: verum
end;
 for x being set st 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  }  holds
x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }
proof
let x be set ; ::_thesis: ( 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  }  implies x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  )
assume A6: 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  }  ; ::_thesis: x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with 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 = x as Attribute of C ;
 for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  implies o is-connected-with x )
assume  o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: o is-connected-with x
then  ex o9 being Object of C st
( o9 = o & ( for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o9 is-connected-with a ) ) ;
hence  o is-connected-with x by A6; ::_thesis: verum
end;
hence  x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: verum
end;
then A7:  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  =  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  by A1, TARSKI:1;
  {  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 x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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  }  or x in the carrier' of C )
assume  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  }  ; ::_thesis: x in the carrier' of C
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  x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A =  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  as Subset of the carrier' of C ;
  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  or x in the carrier of C )
assume  x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: x in the carrier of C
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  x in the carrier of C ; ::_thesis: verum
end;
then reconsider O9 =  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a  }  holds
o is-connected-with a  }  as Subset of the carrier of C ;
 ( A = (ObjectDerivation C) . O & O9 = (AttributeDerivation C) . A ) by Def3, Def4;
hence  (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O)) by A7, Def3; ::_thesis: verum
end;

theorem Th8: :: CONLAT_1:8
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; ::_thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
let A be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  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 where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  ;
A1: for x being set st x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
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  }
proof
let x be set ; ::_thesis: ( x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  implies 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  }  )
assume  x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: 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  }
then A2: ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
x9 is-connected-with a ) ) ;
then reconsider x = 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; ::_thesis: ( a in A implies x is-connected-with a )
assume A3: a in A ; ::_thesis: x is-connected-with a
now__::_thesis:_(_(_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in_A_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_x_is-connected-with_a_)_or_(_not_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in_A_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_x_is-connected-with_a_)_)
percases ( a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  or not a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  ) ;
case a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: x is-connected-with a
hence  x is-connected-with a by A2; ::_thesis: verum
end;
case not a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: x is-connected-with a
then consider o being Object of C such that
A4: o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  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  x is-connected-with a by A3, A5; ::_thesis: verum
end;
end;
end;
hence  x is-connected-with a ; ::_thesis: verum
end;
hence  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  }  ; ::_thesis: verum
end;
 for x being set st 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  }  holds
x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }
proof
let x be set ; ::_thesis: ( 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  }  implies x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  )
assume 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  }  ; ::_thesis: x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }
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 = x as Object of C ;
 for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  implies x is-connected-with a )
assume  a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: x is-connected-with a
then  ex a9 being Attribute of C st
( a9 = a & ( for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a9 ) ) ;
hence  x is-connected-with a by A6; ::_thesis: verum
end;
hence  x in  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: verum
end;
then A7:  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  =  {  o where o is Object of C : for a being Attribute of C st a in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  holds
o is-connected-with a  }  by A1, TARSKI:1;
  {  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 x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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  }  or x in the carrier of C )
assume  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  }  ; ::_thesis: x in the carrier of C
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  x in the carrier of C ; ::_thesis: verum
end;
then reconsider O =  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  as Subset of the carrier of C ;
  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  or x in the carrier' of C )
assume  x in  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  ; ::_thesis: x in the carrier' of C
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  x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A9 =  {  a where a is Attribute of C : for o being Object of C st o in  {  o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a  }  holds
o is-connected-with a  }  as Subset of the carrier' of C ;
 ( O = (AttributeDerivation C) . A & A9 = (ObjectDerivation C) . O ) by Def3, Def4;
hence  (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A)) by A7, Def4; ::_thesis: verum
end;

theorem Th9: :: CONLAT_1:9
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; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds
( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )
let A be Subset of the carrier' of C; ::_thesis: ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information 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 ; ::_thesis: O c= (AttributeDerivation C) . A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O or x in (AttributeDerivation C) . A )
assume A3: x in O ; ::_thesis: x in (AttributeDerivation C) . A
then reconsider x = 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; ::_thesis: ( a in A implies x is-connected-with a )
consider z being set  such that
A4: z = [x,a] ;
assume  a in A ; ::_thesis: x is-connected-with a
then  z in [:O,A:] by A3, A4, ZFMISC_1:def_2;
hence  x is-connected-with a by A2, A4, Def2; ::_thesis: verum
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  x in (AttributeDerivation C) . A by Def4; ::_thesis: verum
end;
 ( O c= (AttributeDerivation C) . A implies [:O,A:] c= the Information of C )
proof
assume  O c= (AttributeDerivation C) . A ; ::_thesis: [:O,A:] c= the Information of C
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 Def4;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:O,A:] or z in the Information of C )
assume  z in [:O,A:] ; ::_thesis: z in the Information of C
then consider x, y being set  such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def_2;
reconsider y = y as Attribute of C by A7;
reconsider x = 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  z in the Information of C by A8, Def2; ::_thesis: verum
end;
hence  ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by A1; ::_thesis: verum
end;

theorem Th10: :: CONLAT_1:10
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; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds
( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )
let A be Subset of the carrier' of C; ::_thesis: ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information 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 ; ::_thesis: A c= (ObjectDerivation C) . O
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (ObjectDerivation C) . O )
assume A3: x in A ; ::_thesis: x in (ObjectDerivation C) . O
then reconsider x = 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; ::_thesis: ( o in O implies o is-connected-with x )
consider z being set  such that
A4: z = [o,x] ;
assume  o in O ; ::_thesis: o is-connected-with x
then  z in [:O,A:] by A3, A4, ZFMISC_1:def_2;
hence  o is-connected-with x by A2, A4, Def2; ::_thesis: verum
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  x in (ObjectDerivation C) . O by Def3; ::_thesis: verum
end;
 ( A c= (ObjectDerivation C) . O implies [:O,A:] c= the Information of C )
proof
assume  A c= (ObjectDerivation C) . O ; ::_thesis: [:O,A:] c= the Information of C
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 Def3;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:O,A:] or z in the Information of C )
assume  z in [:O,A:] ; ::_thesis: z in the Information of C
then consider x, y being set  such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def_2;
reconsider y = y as Attribute of C by A7;
reconsider x = 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  z in the Information of C by A8, Def2; ::_thesis: verum
end;
hence  ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C ) by A1; ::_thesis: verum
end;

theorem :: CONLAT_1:11
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; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
let A be Subset of the carrier' of C; ::_thesis: ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
 ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by Th9;
hence  ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O ) by Th10; ::_thesis: verum
end;

definition
let C be FormalContext;
func phi C ->  Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) equals :: CONLAT_1:def 5
 ObjectDerivation C;
coherence
 ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C)
proof
A1: rng (ObjectDerivation C) c= the carrier of (BoolePoset the carrier' of C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (ObjectDerivation C) or x in the carrier of (BoolePoset the carrier' of C) )
assume  x in rng (ObjectDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier' of 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  x in the carrier of (BoolePoset the carrier' of C) by A2, YELLOW_1:def_2; ::_thesis: verum
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 set st x in the carrier of (BoolePoset the carrier of C) holds
x in dom (ObjectDerivation C)
proof
let x be set ; ::_thesis: ( x in the carrier of (BoolePoset the carrier of C) implies x in dom (ObjectDerivation C) )
assume  x in the carrier of (BoolePoset the carrier of C) ; ::_thesis: x in dom (ObjectDerivation 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  x in dom (ObjectDerivation C) by FUNCT_2:def_1; ::_thesis: verum
end;
 for x being set st x in dom (ObjectDerivation C) holds
x in the carrier of (BoolePoset the carrier of C)
proof
let x be set ; ::_thesis: ( x in dom (ObjectDerivation C) implies x in the carrier of (BoolePoset the carrier of C) )
assume  x in dom (ObjectDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier of 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  x in the carrier of (BoolePoset the carrier of C) by A3, YELLOW_1:def_2; ::_thesis: verum
end;
then  dom (ObjectDerivation C) = the carrier of (BoolePoset the carrier of C) by A4, TARSKI:1;
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  ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) ; ::_thesis: verum
end;
end;

:: deftheorem  defines phi CONLAT_1:def_5_:_
 for C being FormalContext holds phi C = ObjectDerivation C;

definition
let C be FormalContext;
func psi C ->  Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) equals :: CONLAT_1:def 6
 AttributeDerivation C;
coherence
 AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C)
proof
A1: rng (AttributeDerivation C) c= the carrier of (BoolePoset the carrier of C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (AttributeDerivation C) or x in the carrier of (BoolePoset the carrier of C) )
assume  x in rng (AttributeDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier of 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  x in the carrier of (BoolePoset the carrier of C) by A2, YELLOW_1:def_2; ::_thesis: verum
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 set st x in the carrier of (BoolePoset the carrier' of C) holds
x in dom (AttributeDerivation C)
proof
let x be set ; ::_thesis: ( x in the carrier of (BoolePoset the carrier' of C) implies x in dom (AttributeDerivation C) )
assume  x in the carrier of (BoolePoset the carrier' of C) ; ::_thesis: x in dom (AttributeDerivation 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  x in dom (AttributeDerivation C) by FUNCT_2:def_1; ::_thesis: verum
end;
 for x being set st x in dom (AttributeDerivation C) holds
x in the carrier of (BoolePoset the carrier' of C)
proof
let x be set ; ::_thesis: ( x in dom (AttributeDerivation C) implies x in the carrier of (BoolePoset the carrier' of C) )
assume  x in dom (AttributeDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier' of 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  x in the carrier of (BoolePoset the carrier' of C) by A3, YELLOW_1:def_2; ::_thesis: verum
end;
then  dom (AttributeDerivation C) = the carrier of (BoolePoset the carrier' of C) by A4, TARSKI:1;
hence  AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

:: deftheorem  defines psi CONLAT_1:def_6_:_
 for C being FormalContext holds psi C = AttributeDerivation C;

definition
let P, R be non empty RelStr ;
let Con be Connection of P,R;
attrCon is co-Galois  means :Def7: :: CONLAT_1:def 7
 ex f being Function of P,R ex g being Function of R,P st
( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) );
end;

:: deftheorem Def7 defines co-Galois CONLAT_1:def_7_:_
 for P, R being non empty RelStr
for Con being Connection of P,R holds
( Con is co-Galois iff ex f being Function of P,R ex g being Function of R,P st
( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ) );

theorem Th12: :: CONLAT_1:12
for P, R being non empty Poset
for Con being Connection of P,R
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
proof
let P, R be non empty Poset; ::_thesis: for Con being Connection of P,R
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let Con be Connection of P,R; ::_thesis: for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let f be Function of P,R; ::_thesis: for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let g be Function of R,P; ::_thesis: ( Con = [f,g] implies ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) )
assume A1: Con = [f,g] ; ::_thesis: ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
A2: now__::_thesis:_(_(_for_p_being_Element_of_P
for_r_being_Element_of_R_holds_
(_p_<=_g_._r_iff_r_<=_f_._p_)_)_implies_Con_is_co-Galois_)
assume A3: for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ; ::_thesis: Con is co-Galois
 for p1, p2 being Element of P st p1 <= p2 holds
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; ::_thesis: ( p1 <= p2 implies for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2 )
assume A4: p1 <= p2 ; ::_thesis: for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2
let r1, r2 be Element of R; ::_thesis: ( r1 = f . p1 & r2 = f . p2 implies r1 >= r2 )
assume A5: ( r1 = f . p1 & r2 = f . p2 ) ; ::_thesis: r1 >= r2
 p2 <= g . (f . p2) by A3;
then  p1 <= g . (f . p2) by A4, ORDERS_2:3;
hence  r1 >= r2 by A3, A5; ::_thesis: verum
end;
then A6: f is antitone by WAYBEL_0:def_5;
 for r1, r2 being Element of R st r1 <= r2 holds
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; ::_thesis: ( r1 <= r2 implies for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2 )
assume A7: r1 <= r2 ; ::_thesis: for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2
let p1, p2 be Element of P; ::_thesis: ( p1 = g . r1 & p2 = g . r2 implies p1 >= p2 )
assume A8: ( p1 = g . r1 & p2 = g . r2 ) ; ::_thesis: p1 >= p2
 r2 <= f . (g . r2) by A3;
then  r1 <= f . (g . r2) by A7, ORDERS_2:3;
hence  p1 >= p2 by A3, A8; ::_thesis: verum
end;
then A9: g is antitone by WAYBEL_0:def_5;
 for p1, p2 being Element of P
for 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, Def7; ::_thesis: verum
end;
now__::_thesis:_(_Con_is_co-Galois_implies_for_p_being_Element_of_P
for_r_being_Element_of_R_holds_
(_p_<=_g_._r_iff_r_<=_f_._p_)_)
assume  Con is co-Galois ; ::_thesis: for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p )
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
for r1, r2 being Element of R holds
( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) by Def7;
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
for r being Element of R st r <= f . p holds
p <= g . r
proof
let p be Element of P; ::_thesis: for r being Element of R st r <= f . p holds
p <= g . r
let r be Element of R; ::_thesis: ( r <= f . p implies p <= g . r )
assume  r <= f . p ; ::_thesis: p <= g . r
then A17: g . r >= g . (f . p) by A12, A14, WAYBEL_0:def_5;
 p <= g . (f . p) by A13, A15, A14;
hence  p <= g . r by A17, ORDERS_2:3; ::_thesis: verum
end;
 for p being Element of P
for r being Element of R st p <= g . r holds
r <= f . p
proof
let p be Element of P; ::_thesis: for r being Element of R st p <= g . r holds
r <= f . p
let r be Element of R; ::_thesis: ( p <= g . r implies r <= f . p )
assume  p <= g . r ; ::_thesis: r <= f . p
then A18: f . p >= f . (g . r) by A11, A15, WAYBEL_0:def_5;
 r <= f . (g . r) by A13, A15, A14;
hence  r <= f . p by A18, ORDERS_2:3; ::_thesis: verum
end;
hence  for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) by A16; ::_thesis: verum
end;
hence  ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) by A2; ::_thesis: verum
end;

theorem :: CONLAT_1:13
for P, R being non empty Poset
for Con being Connection of P,R st Con is co-Galois holds
for f being Function of P,R
for 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; ::_thesis: for Con being Connection of P,R st Con is co-Galois holds
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let Con be Connection of P,R; ::_thesis: ( Con is co-Galois implies for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) ) )
assume  Con is co-Galois ; ::_thesis: for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
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
for r1, r2 being Element of R holds
( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) by Def7;
let f be Function of P,R; ::_thesis: for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let g be Function of R,P; ::_thesis: ( Con = [f,g] implies ( f = f * (g * f) & g = g * (f * g) ) )
assume A5: Con = [f,g] ; ::_thesis: ( f = f * (g * f) & g = g * (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 set st x in the carrier of P holds
f . x = (f * (g * f)) . x
proof
let x be set ; ::_thesis: ( x in the carrier of P implies f . x = (f * (g * f)) . x )
assume  x in the carrier of P ; ::_thesis: f . x = (f * (g * f)) . x
then reconsider x = 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  f . x = (f * (g * f)) . x by A12, FUNCT_1:13; ::_thesis: verum
end;
A13: for x being set st x in the carrier of R holds
g . x = (g * (f * g)) . x
proof
let x be set ; ::_thesis: ( x in the carrier of R implies g . x = (g * (f * g)) . x )
assume  x in the carrier of R ; ::_thesis: g . x = (g * (f * g)) . x
then reconsider x = 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  g . x = (g * (f * g)) . x by A15, FUNCT_1:13; ::_thesis: verum
end;
 ( dom (f * (g * f)) = the carrier of P & dom (g * (f * g)) = the carrier of R ) by FUNCT_2:def_1;
hence  ( f = f * (g * f) & g = g * (f * g) ) by A9, A8, A10, A13, FUNCT_1:2; ::_thesis: verum
end;

theorem :: CONLAT_1:14
for C being FormalContext holds [(phi C),(psi C)] is co-Galois
proof
let C be FormalContext; ::_thesis: [(phi C),(psi C)] is co-Galois
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)
for 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); ::_thesis: for y being Element of (BoolePoset the carrier' of C) st y <= (phi C) . x holds
x <= (psi C) . y
let y be Element of (BoolePoset the carrier' of C); ::_thesis: ( y <= (phi C) . x implies x <= (psi C) . y )
assume  y <= (phi C) . x ; ::_thesis: x <= (psi C) . y
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 = x as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def_2;
reconsider x = x as Subset of the carrier of C by LATTICE3:def_1;
reconsider y = 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 = x9 as Subset of the carrier' of C by LATTICE3:def_1;
reconsider y = y as Subset of the carrier' of C by LATTICE3:def_1;
 for z being set st z in y holds
z in x9 by A5, XBOOLE_0:def_3;
then  y c= x9 by TARSKI:def_3;
then A6: (AttributeDerivation C) . x9 c= (AttributeDerivation C) . y by Th4;
reconsider y = 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 = y9 as Subset of the carrier of C by LATTICE3:def_1;
reconsider y9 = y9 as Element of (BooleLatt the carrier of C) ;
A7: x c= (AttributeDerivation C) . ((ObjectDerivation C) . x) by Th5;
reconsider x = x as Subset of the carrier of C ;
reconsider x = x as Element of (BooleLatt the carrier of C) ;
 x "\/" y9 = y9 by A6, A7, XBOOLE_1:1, XBOOLE_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  x <= (psi C) . y by ORDERS_2:def_5; ::_thesis: verum
end;
 for x being Element of (BoolePoset the carrier of C)
for 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); ::_thesis: for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds
y <= (phi C) . x
let y be Element of (BoolePoset the carrier' of C); ::_thesis: ( x <= (psi C) . y implies y <= (phi C) . x )
assume  x <= (psi C) . y ; ::_thesis: y <= (phi C) . x
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 = y as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2;
reconsider y = y as Subset of the carrier' of C by LATTICE3:def_1;
reconsider x = 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 = y9 as Subset of the carrier of C by LATTICE3:def_1;
reconsider x = x as Subset of the carrier of C by LATTICE3:def_1;
 for z being set st z in x holds
z in y9 by A9, XBOOLE_0:def_3;
then A10: x c= y9 by TARSKI:def_3;
reconsider x = x, y9 = y9 as Subset of the carrier of C ;
A11: (ObjectDerivation C) . y9 c= (ObjectDerivation C) . x by A10, Th3;
reconsider x = 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 = x9 as Subset of the carrier' of C by LATTICE3:def_1;
reconsider x9 = x9 as Element of (BooleLatt the carrier' of C) ;
A12: y c= (ObjectDerivation C) . ((AttributeDerivation C) . y) by Th6;
reconsider y = y as Element of (BooleLatt the carrier' of C) ;
 y "\/" x9 = x9 by A11, A12, XBOOLE_1:1, XBOOLE_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  y <= (phi C) . x by ORDERS_2:def_5; ::_thesis: verum
end;
hence  [(phi C),(psi C)] is co-Galois by A3, Th12; ::_thesis: verum
end;

theorem Th15: :: CONLAT_1:15
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; ::_thesis: for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
let O1, O2 be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
reconsider O9 = O1 \/ O2 as Subset of the carrier of C ;
A1: for x being set st x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) holds
x in (ObjectDerivation C) . O9
proof
let x be set ; ::_thesis: ( x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) implies x in (ObjectDerivation C) . O9 )
assume A2: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) ; ::_thesis: x in (ObjectDerivation C) . O9
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 Def3;
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 Def3;
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 = 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; ::_thesis: ( o in O1 \/ O2 implies o is-connected-with x )
assume A5: o in O1 \/ O2 ; ::_thesis: o is-connected-with x
now__::_thesis:_(_(_o_in_O1_&_o_is-connected-with_x_)_or_(_o_in_O2_&_o_is-connected-with_x_)_)
percases ( o in O1 or o in O2 ) by A5, XBOOLE_0:def_3;
case o in O1 ; ::_thesis: o is-connected-with x
hence  o is-connected-with x by A3; ::_thesis: verum
end;
case o in O2 ; ::_thesis: o is-connected-with x
hence  o is-connected-with x by A4; ::_thesis: verum
end;
end;
end;
hence  o is-connected-with x ; ::_thesis: verum
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  x in (ObjectDerivation C) . O9 by Def3; ::_thesis: verum
end;
 for x being set st x in (ObjectDerivation C) . (O1 \/ O2) holds
x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
proof
let x be set ; ::_thesis: ( x in (ObjectDerivation C) . (O1 \/ O2) implies x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) )
assume  x in (ObjectDerivation C) . (O1 \/ O2) ; ::_thesis: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . 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 Def3;
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 = 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; ::_thesis: ( o in O2 implies o is-connected-with x )
assume  o in O2 ; ::_thesis: o is-connected-with x
then  o in O9 by XBOOLE_0:def_3;
hence  o is-connected-with x by A6; ::_thesis: verum
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 Def3;
 for o being Object of C st o in O1 holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O1 implies o is-connected-with x )
assume  o in O1 ; ::_thesis: o is-connected-with x
then  o in O9 by XBOOLE_0:def_3;
hence  o is-connected-with x by A6; ::_thesis: verum
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 Def3;
hence  x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A1, TARSKI:1; ::_thesis: verum
end;

theorem Th16: :: CONLAT_1:16
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; ::_thesis: for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
let A1, A2 be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
reconsider A9 = A1 \/ A2 as Subset of the carrier' of C ;
A1: for x being set st x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) holds
x in (AttributeDerivation C) . A9
proof
let x be set ; ::_thesis: ( x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) implies x in (AttributeDerivation C) . A9 )
assume A2: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) ; ::_thesis: x in (AttributeDerivation C) . A9
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 Def4;
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 Def4;
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 = 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; ::_thesis: ( a in A1 \/ A2 implies x is-connected-with a )
assume A5: a in A1 \/ A2 ; ::_thesis: x is-connected-with a
now__::_thesis:_(_(_a_in_A1_&_x_is-connected-with_a_)_or_(_a_in_A2_&_x_is-connected-with_a_)_)
percases ( a in A1 or a in A2 ) by A5, XBOOLE_0:def_3;
case a in A1 ; ::_thesis: x is-connected-with a
hence  x is-connected-with a by A3; ::_thesis: verum
end;
case a in A2 ; ::_thesis: x is-connected-with a
hence  x is-connected-with a by A4; ::_thesis: verum
end;
end;
end;
hence  x is-connected-with a ; ::_thesis: verum
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  x in (AttributeDerivation C) . A9 by Def4; ::_thesis: verum
end;
 for x being set st x in (AttributeDerivation C) . (A1 \/ A2) holds
x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
proof
let x be set ; ::_thesis: ( x in (AttributeDerivation C) . (A1 \/ A2) implies x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) )
assume  x in (AttributeDerivation C) . (A1 \/ A2) ; ::_thesis: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . 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 Def4;
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 = 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; ::_thesis: ( a in A2 implies x is-connected-with a )
assume  a in A2 ; ::_thesis: x is-connected-with a
then  a in A9 by XBOOLE_0:def_3;
hence  x is-connected-with a by A6; ::_thesis: verum
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 Def4;
 for a being Attribute of C st a in A1 holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A1 implies x is-connected-with a )
assume  a in A1 ; ::_thesis: x is-connected-with a
then  a in A9 by XBOOLE_0:def_3;
hence  x is-connected-with a by A6; ::_thesis: verum
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 Def4;
hence  x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A1, TARSKI:1; ::_thesis: verum
end;

theorem Th17: :: CONLAT_1:17
for C being FormalContext holds (ObjectDerivation C) . {} = the carrier' of C
proof
let C be FormalContext; ::_thesis: (ObjectDerivation C) . {} = the carrier' of C
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 set st x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }  holds
x in the carrier' of C
proof
let x be set ; ::_thesis: ( x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }  implies x in the carrier' of C )
assume  x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }  ; ::_thesis: x in the carrier' of C
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  x in the carrier' of C ; ::_thesis: verum
end;
A2: for x being set st x in the carrier' of C holds
x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }
proof
let x be set ; ::_thesis: ( x in the carrier' of C implies x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }  )
assume  x in the carrier' of C ; ::_thesis: x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }
then reconsider x = x as Attribute of C ;
 for o being Object of C st o in e holds
o is-connected-with x ;
hence  x in  {  a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a  }  ; ::_thesis: verum
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 Def3;
hence  (ObjectDerivation C) . {} = the carrier' of C by A1, A2, TARSKI:1; ::_thesis: verum
end;

theorem Th18: :: CONLAT_1:18
for C being FormalContext holds (AttributeDerivation C) . {} = the carrier of C
proof
let C be FormalContext; ::_thesis: (AttributeDerivation C) . {} = the carrier of C
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 set st x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }  holds
x in the carrier of C
proof
let x be set ; ::_thesis: ( x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }  implies x in the carrier of C )
assume  x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }  ; ::_thesis: x in the carrier of C
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  x in the carrier of C ; ::_thesis: verum
end;
A2: for x being set st x in the carrier of C holds
x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }
proof
let x be set ; ::_thesis: ( x in the carrier of C implies x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }  )
assume  x in the carrier of C ; ::_thesis: x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }
then reconsider x = x as Object of C ;
 for a being Attribute of C st a in e holds
x is-connected-with a ;
hence  x in  {  o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a  }  ; ::_thesis: verum
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 Def4;
hence  (AttributeDerivation C) . {} = the carrier of C by A1, A2, TARSKI:1; ::_thesis: verum
end;

begin

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

definition
let C be 2-sorted ;
let CP be ConceptStr over C;
attrCP is empty  means :Def8: :: CONLAT_1:def 8
( the Extent of CP is empty & the Intent of CP is empty );
attrCP is quasi-empty  means :Def9: :: CONLAT_1:def 9
( the Extent of CP is empty or the Intent of CP is empty );
end;

:: deftheorem Def8 defines empty CONLAT_1:def_8_:_
 for C being 2-sorted
for CP being ConceptStr over C holds
( CP is empty iff ( the Extent of CP is empty & the Intent of CP is empty ) );

:: deftheorem Def9 defines quasi-empty CONLAT_1:def_9_:_
 for C being 2-sorted
for CP being ConceptStr over C holds
( CP is quasi-empty iff ( the Extent of CP is empty or the Intent of CP is empty ) );

registration
let C be non quasi-empty 2-sorted ;
cluster strict non empty for ConceptStr over C;
existence
 ex b1 being ConceptStr over C st
( b1 is strict & not b1 is empty )
proof
set A = the non empty Subset of the carrier' of C;
set O = the non empty Subset of the carrier of C;
 not ConceptStr(# the non empty Subset of the carrier of C, the non empty Subset of the carrier' of C #) is empty by Def8;
hence  ex b1 being ConceptStr over C st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
cluster strict quasi-empty for ConceptStr over C;
existence
 ex b1 being ConceptStr over C st
( b1 is strict & b1 is quasi-empty )
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 by Def9;
hence  ex b1 being ConceptStr over C st
( b1 is strict & b1 is quasi-empty ) ; ::_thesis: verum
end;
end;

registration
let C be empty void 2-sorted ;
cluster  ->  empty for ConceptStr over C;
coherence
 for b1 being ConceptStr over C holds b1 is empty
proof
let CP be ConceptStr over C; ::_thesis: CP is empty
 ( the Extent of CP is empty & the Intent of CP is empty ) ;
hence  CP is empty by Def8; ::_thesis: verum
end;
end;

registration
let C be quasi-empty 2-sorted ;
cluster  ->  quasi-empty for ConceptStr over C;
coherence
 for b1 being ConceptStr over C holds b1 is quasi-empty
proof
let CP be ConceptStr over C; ::_thesis: CP is quasi-empty
 ( the Extent of CP is empty or the Intent of CP is empty )
proof
set x = the Element of the Extent of CP;
assume  not the Extent of CP is empty ; ::_thesis: the Intent of CP is empty
then A1: the Element of the Extent of CP in the Extent of CP ;
thus  the Intent of CP is empty ::_thesis: verum
proof
set x = the Element of the Intent of CP;
assume  not the Intent of CP is empty ; ::_thesis: contradiction
then  the Element of the Intent of CP in the Intent of CP ;
hence  contradiction by A1, Def1; ::_thesis: verum
end;
end;
hence  CP is quasi-empty by Def9; ::_thesis: verum
end;
end;

Lm1:  for C being FormalContext
for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
proof
let C be FormalContext; ::_thesis: for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
let CS be ConceptStr over C; ::_thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS implies not CS is empty )
assume A1: (ObjectDerivation C) . the Extent of CS = the Intent of CS ; ::_thesis: not CS is empty
now__::_thesis:_(_(_the_Extent_of_CS_is_empty_&_not_CS_is_empty_)_or_(_not_the_Extent_of_CS_is_empty_&_not_CS_is_empty_)_)
percases ( the Extent of CS is empty or not the Extent of CS is empty ) ;
case the Extent of CS is empty ; ::_thesis: not CS is empty
then  the Intent of CS = the carrier' of C by A1, Th17;
hence  not CS is empty by Def8; ::_thesis: verum
end;
case not the Extent of CS is empty ; ::_thesis: not CS is empty
hence  not CS is empty by Def8; ::_thesis: verum
end;
end;
end;
hence  not CS is empty ; ::_thesis: verum
end;

definition
let C be FormalContext;
let CP be ConceptStr over C;
attrCP is concept-like  means :Def10: :: CONLAT_1:def 10
( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP );
end;

:: deftheorem Def10 defines concept-like CONLAT_1:def_10_:_
 for C being FormalContext
for CP being ConceptStr over C holds
( CP is concept-like iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) );

registration
let C be FormalContext;
cluster non empty concept-like for ConceptStr over C;
existence
 ex b1 being ConceptStr over C st
( b1 is concept-like & not b1 is empty )
proof
set o = the Object of C;
set A = (ObjectDerivation C) . { the Object of C};
 { the Object of C} c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { the Object of C} or x in the carrier of C )
assume  x in { the Object of C} ; ::_thesis: x in the carrier of C
then  x = the Object of C by TARSKI:def_1;
hence  x in the carrier of C ; ::_thesis: verum
end;
then reconsider t = { the Object of C} as Subset of the carrier of C ;
 (ObjectDerivation C) . { the Object of C} c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . { the Object of C} or x in the carrier' of C )
assume  x in (ObjectDerivation C) . { the Object of C} ; ::_thesis: x in the carrier' of C
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 Def3;
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  x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = (ObjectDerivation C) . { the Object of C} as Subset of the carrier' of C ;
set O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C});
 (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) or x in the carrier of C )
assume  x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) ; ::_thesis: x in the carrier of C
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 Def4;
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  x in the carrier of C ; ::_thesis: verum
end;
then reconsider O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) as Subset of the carrier of C ;
set M9 = ConceptStr(# O,A #);
 ( the Object of C in { the Object of C} & t c= (AttributeDerivation C) . ((ObjectDerivation C) . t) ) by Th5, TARSKI:def_1;
then reconsider M9 = ConceptStr(# O,A #) as non empty ConceptStr over C by Def8;
(ObjectDerivation C) . the Extent of M9 = (ObjectDerivation C) . t by Th7
.= the Intent of M9 ;
then  M9 is concept-like by Def10;
hence  ex b1 being ConceptStr over C st
( b1 is concept-like & not b1 is empty ) ; ::_thesis: verum
end;
end;

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

registration
let C be FormalContext;
cluster strict non empty concept-like for ConceptStr over C;
existence
 ex b1 being FormalConcept of C st b1 is strict
proof
set CP = the FormalConcept of C;
A1: ( (ObjectDerivation C) . the Extent of the FormalConcept of C = the Intent of the FormalConcept of C & (AttributeDerivation C) . the Intent of the FormalConcept of C = the Extent of the FormalConcept of C ) by Def10;
 ( not the Intent of the FormalConcept of C is empty or not the Extent of the FormalConcept of C is empty ) by Def8;
then  ConceptStr(# the Extent of the FormalConcept of C, the Intent of the FormalConcept of C #) is FormalConcept of C by A1, Def8, Def10;
hence  ex b1 being FormalConcept of C st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th19: :: CONLAT_1:19
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
for 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; ::_thesis: 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
for 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 ) )
let O be Subset of the carrier of C; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C
for 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 ) )
A1: for O9 being Subset of the carrier of C
for 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; ::_thesis: for 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
let A9 be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 implies (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 )
assume that
A2: ConceptStr(# O9,A9 #) is FormalConcept of C and
A3: O c= O9 ; ::_thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9
reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2;
A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def10
.= O9 ;
A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def10
.= A9 ;
 (ObjectDerivation C) . O9 c= (ObjectDerivation C) . O by A3, Th3;
hence  (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 by A4, A5, Th4; ::_thesis: verum
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 ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) = the Intent of ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) by Th7;
hence  ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C by Def10, Lm1; ::_thesis: verum
end;
hence  ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C
for 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 ) ) by A1; ::_thesis: verum
end;

theorem :: CONLAT_1:20
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; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: ( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O )
A1: now__::_thesis:_(_ex_A_being_Subset_of_the_carrier'_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_implies_(AttributeDerivation_C)_._((ObjectDerivation_C)_._O)_=_O_)
 O c= (AttributeDerivation C) . ((ObjectDerivation C) . O) by Th5;
then A2: for x being set st x in O holds
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 ; ::_thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) = O
 (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O by A3, Th19;
then  for x being set st x in (AttributeDerivation C) . ((ObjectDerivation C) . O) holds
x in O ;
hence  (AttributeDerivation C) . ((ObjectDerivation C) . O) = O by A2, TARSKI:1; ::_thesis: verum
end;
now__::_thesis:_(_(AttributeDerivation_C)_._((ObjectDerivation_C)_._O)_=_O_implies_ex_A_being_Subset_of_the_carrier'_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_)
reconsider A = (ObjectDerivation C) . O as Subset of the carrier' of C ;
set M9 = ConceptStr(# O,A #);
assume  (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ; ::_thesis: ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C
then  ConceptStr(# O,A #) is FormalConcept of C by Def10, Lm1;
hence  ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: verum
end;
hence  ( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ) by A1; ::_thesis: verum
end;

theorem Th21: :: CONLAT_1:21
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
for 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; ::_thesis: 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
for 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 ) )
let A be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C
for 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 ) )
A1: for O9 being Subset of the carrier of C
for 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; ::_thesis: for 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
let A9 be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & A c= A9 implies (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 )
assume that
A2: ConceptStr(# O9,A9 #) is FormalConcept of C and
A3: A c= A9 ; ::_thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9
reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2;
A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def10
.= O9 ;
A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def10
.= A9 ;
 (AttributeDerivation C) . A9 c= (AttributeDerivation C) . A by A3, Th4;
hence  (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 by A4, A5, Th3; ::_thesis: verum
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 ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) = the Extent of ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) by Th8;
hence  ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C by Def10, Lm1; ::_thesis: verum
end;
hence  ( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C
for 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 ) ) by A1; ::_thesis: verum
end;

theorem :: CONLAT_1:22
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; ::_thesis: 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 )
let A be Subset of the carrier' of C; ::_thesis: ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )
A1: now__::_thesis:_(_ex_O_being_Subset_of_the_carrier_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_implies_(ObjectDerivation_C)_._((AttributeDerivation_C)_._A)_=_A_)
 A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) by Th6;
then A2: for x being set st x in A holds
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 ; ::_thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) = A
 (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A by A3, Th21;
then  for x being set st x in (ObjectDerivation C) . ((AttributeDerivation C) . A) holds
x in A ;
hence  (ObjectDerivation C) . ((AttributeDerivation C) . A) = A by A2, TARSKI:1; ::_thesis: verum
end;
now__::_thesis:_(_(ObjectDerivation_C)_._((AttributeDerivation_C)_._A)_=_A_implies_ex_O_being_Subset_of_the_carrier_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_)
reconsider O = (AttributeDerivation C) . A as Subset of the carrier of C ;
set M9 = ConceptStr(# O,A #);
assume  (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ; ::_thesis: ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C
then  ConceptStr(# O,A #) is FormalConcept of C by Def10, Lm1;
hence  ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: verum
end;
hence  ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ) by A1; ::_thesis: verum
end;

definition
let C be FormalContext;
let CP be ConceptStr over C;
attrCP is universal  means :Def11: :: CONLAT_1:def 11
 the Extent of CP = the carrier of C;
end;

:: deftheorem Def11 defines universal CONLAT_1:def_11_:_
 for C being FormalContext
for CP being ConceptStr over C holds
( CP is universal iff the Extent of CP = the carrier of C );

definition
let C be FormalContext;
let CP be ConceptStr over C;
attrCP is co-universal  means :Def12: :: CONLAT_1:def 12
 the Intent of CP = the carrier' of C;
end;

:: deftheorem Def12 defines co-universal CONLAT_1:def_12_:_
 for C being FormalContext
for CP being ConceptStr over C holds
( CP is co-universal iff the Intent of CP = the carrier' of C );

registration
let C be FormalContext;
cluster strict non empty concept-like universal for ConceptStr over C;
existence
 ex b1 being FormalConcept of C st
( b1 is strict & b1 is universal )
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 by Def11;
hence  ex b1 being FormalConcept of C st
( b1 is strict & b1 is universal ) ; ::_thesis: verum
end;
cluster strict non empty concept-like co-universal for ConceptStr over C;
existence
 ex b1 being FormalConcept of C st
( b1 is strict & b1 is co-universal )
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 by Def12;
hence  ex b1 being FormalConcept of C st
( b1 is strict & b1 is co-universal ) ; ::_thesis: verum
end;
end;

definition
let C be FormalContext;
func Concept-with-all-Objects C ->  strict universal FormalConcept of C means :Def13: :: CONLAT_1:def 13
 ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) );
existence
 ex b1 being strict universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) )
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 by Def11;
hence  ex b1 being strict universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) & ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) holds
b1 = b2 ;
end;

:: deftheorem Def13 defines Concept-with-all-Objects CONLAT_1:def_13_:_
 for C being FormalContext
for b2 being strict universal FormalConcept of C holds
( b2 = Concept-with-all-Objects C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) );

definition
let C be FormalContext;
func Concept-with-all-Attributes C ->  strict co-universal FormalConcept of C means :Def14: :: CONLAT_1:def 14
 ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} );
existence
 ex b1 being strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} )
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 by Def12;
hence  ex b1 being strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict co-universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) & ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) holds
b1 = b2 ;
end;

:: deftheorem Def14 defines Concept-with-all-Attributes CONLAT_1:def_14_:_
 for C being FormalContext
for b2 being strict co-universal FormalConcept of C holds
( b2 = Concept-with-all-Attributes C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) );

theorem Th23: :: CONLAT_1:23
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; ::_thesis: ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C )
 ( ex O being Subset of the carrier of C ex 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 ex 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 Def13, Def14;
hence  ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C ) by Th17, Th18; ::_thesis: verum
end;

theorem :: CONLAT_1:24
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; ::_thesis: for CP being FormalConcept of C holds
( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )
let CP be FormalConcept of C; ::_thesis: ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10;
A2: now__::_thesis:_(_the_Intent_of_CP_=_{}_implies_CP_is_universal_)
assume  the Intent of CP = {} ; ::_thesis: CP is universal
then  the Extent of CP = the carrier of C by A1, Th18;
hence  CP is universal by Def11; ::_thesis: verum
end;
A3: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10;
now__::_thesis:_(_the_Extent_of_CP_=_{}_implies_CP_is_co-universal_)
assume  the Extent of CP = {} ; ::_thesis: CP is co-universal
then  the Intent of CP = the carrier' of C by A3, Th17;
hence  CP is co-universal by Def12; ::_thesis: verum
end;
hence  ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) by A2; ::_thesis: verum
end;

theorem Th25: :: CONLAT_1:25
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; ::_thesis: 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 ) )
let CP be strict FormalConcept of C; ::_thesis: ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) )
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10;
A3: now__::_thesis:_(_the_Intent_of_CP_=_{}_implies_CP_=_Concept-with-all-Objects_C_)
assume A4: the Intent of CP = {} ; ::_thesis: CP = Concept-with-all-Objects C
then  the Extent of CP = the carrier of C by A1, Th18;
then  CP is universal by Def11;
hence  CP = Concept-with-all-Objects C by A2, A1, A4, Def13; ::_thesis: verum
end;
now__::_thesis:_(_the_Extent_of_CP_=_{}_implies_CP_=_Concept-with-all-Attributes_C_)
assume A5: the Extent of CP = {} ; ::_thesis: CP = Concept-with-all-Attributes C
then  the Intent of CP = the carrier' of C by A2, Th17;
then  CP is co-universal by Def12;
hence  CP = Concept-with-all-Attributes C by A2, A1, A5, Def14; ::_thesis: verum
end;
hence  ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) ) by A3; ::_thesis: verum
end;

theorem :: CONLAT_1:26
for C being FormalContext
for CP being quasi-empty ConceptStr over C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )
proof
let C be FormalContext; ::_thesis: for CP being quasi-empty ConceptStr over C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )
let CP be quasi-empty ConceptStr over C; ::_thesis: ( not CP is FormalConcept of C or CP is universal or CP is co-universal )
assume  CP is FormalConcept of C ; ::_thesis: ( CP is universal or CP is co-universal )
then reconsider CP = CP as FormalConcept of C ;
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10;
now__::_thesis:_(_(_the_Intent_of_CP_is_empty_&_CP_is_universal_)_or_(_the_Extent_of_CP_is_empty_&_CP_is_co-universal_)_)
percases ( the Intent of CP is empty or the Extent of CP is empty ) by Def9;
case the Intent of CP is empty ; ::_thesis: CP is universal
then  the Extent of CP = the carrier of C by A1, Th18;
hence  CP is universal by Def11; ::_thesis: verum
end;
case the Extent of CP is empty ; ::_thesis: CP is co-universal
then  the Intent of CP = the carrier' of C by A2, Th17;
hence  CP is co-universal by Def12; ::_thesis: verum
end;
end;
end;
hence  ( CP is universal or CP is co-universal ) ; ::_thesis: verum
end;

theorem :: CONLAT_1:27
for C being FormalContext
for CP being quasi-empty ConceptStr over C holds
( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
proof
let C be FormalContext; ::_thesis: for CP being quasi-empty ConceptStr over C holds
( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
let CP be quasi-empty ConceptStr over C; ::_thesis: ( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
assume A1: CP is strict FormalConcept of C ; ::_thesis: ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
now__::_thesis:_(_(_the_Intent_of_CP_is_empty_&_CP_=_Concept-with-all-Objects_C_)_or_(_the_Extent_of_CP_is_empty_&_CP_=_Concept-with-all-Attributes_C_)_)
percases ( the Intent of CP is empty or the Extent of CP is empty ) by Def9;
case the Intent of CP is empty ; ::_thesis: CP = Concept-with-all-Objects C
hence  CP = Concept-with-all-Objects C by A1, Th25; ::_thesis: verum
end;
case the Extent of CP is empty ; ::_thesis: CP = Concept-with-all-Attributes C
hence  CP = Concept-with-all-Attributes C by A1, Th25; ::_thesis: verum
end;
end;
end;
hence  ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) ; ::_thesis: verum
end;

definition
let C be FormalContext;
mode Set-of-FormalConcepts of C ->  non empty set  means :Def15: :: CONLAT_1:def 15
 for X being set st X in it holds
X is FormalConcept of C;
existence
 ex b1 being non empty set st
for X being set st X in b1 holds
X is FormalConcept of C
proof
set CP = the FormalConcept of C;
 for X being set st X in { the FormalConcept of C} holds
X is FormalConcept of C by TARSKI:def_1;
hence  ex b1 being non empty set st
for X being set st X in b1 holds
X is FormalConcept of C ; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines Set-of-FormalConcepts CONLAT_1:def_15_:_
 for C being FormalContext
for b2 being non empty set holds
( b2 is Set-of-FormalConcepts of C iff for X being set st X in b2 holds
X is FormalConcept of C );

definition
let C be FormalContext;
let FCS be Set-of-FormalConcepts of C;
:: original: Element
redefine mode Element of FCS ->  FormalConcept of C;
coherence
 for b1 being Element of FCS holds b1 is FormalConcept of C by Def15;
end;

definition
let C be FormalContext;
let CP1, CP2 be FormalConcept of C;
predCP1 is-SubConcept-of CP2 means :Def16: :: CONLAT_1:def 16
 the Extent of CP1 c= the Extent of CP2;
end;

:: deftheorem Def16 defines is-SubConcept-of CONLAT_1:def_16_:_
 for C being FormalContext
for CP1, CP2 being FormalConcept of C holds
( CP1 is-SubConcept-of CP2 iff the Extent of CP1 c= the Extent of CP2 );

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: :: CONLAT_1:28
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; ::_thesis: for CP1, CP2 being FormalConcept of C holds
( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )
let CP1, CP2 be FormalConcept of C; ::_thesis: ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )
A1: now__::_thesis:_(_the_Intent_of_CP2_c=_the_Intent_of_CP1_implies_CP1_is-SubConcept-of_CP2_)
assume  the Intent of CP2 c= the Intent of CP1 ; ::_thesis: CP1 is-SubConcept-of CP2
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 Def10;
hence  CP1 is-SubConcept-of CP2 by A2, Def16; ::_thesis: verum
end;
now__::_thesis:_(_CP1_is-SubConcept-of_CP2_implies_the_Intent_of_CP2_c=_the_Intent_of_CP1_)
assume  CP1 is-SubConcept-of CP2 ; ::_thesis: the Intent of CP2 c= the Intent of CP1
then A3: the Extent of CP1 c= the Extent of CP2 by Def16;
 ( (ObjectDerivation C) . the Extent of CP2 = the Intent of CP2 & (ObjectDerivation C) . the Extent of CP1 = the Intent of CP1 ) by Def10;
hence  the Intent of CP2 c= the Intent of CP1 by A3, Th3; ::_thesis: verum
end;
hence  ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 ) by A1; ::_thesis: verum
end;

theorem :: CONLAT_1:29
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 :: CONLAT_1:30
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; ::_thesis: 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 )
let CP be FormalConcept of C; ::_thesis: ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP )
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  ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP ) by A1, Def16, Th28; ::_thesis: verum
end;

begin

definition
let C be FormalContext;
func B-carrier C ->  non empty set  equals :: CONLAT_1:def 17
 {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  ;
coherence
  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  is non empty set
proof
set M9 =  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  ;
 not  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  is empty
proof
set CP = the FormalConcept of C;
consider O being Subset of the carrier of C such that
A1: O = the Extent of the FormalConcept of C ;
consider A being Subset of the carrier' of C such that
A2: A = the Intent of the FormalConcept of C ;
A3: (AttributeDerivation C) . A = O by A1, A2, Def10;
A4: (ObjectDerivation C) . O = A by A1, A2, Def10;
then  not ConceptStr(# O,A #) is empty by Lm1;
then  ConceptStr(# O,A #) in  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  by A4, A3;
hence  not  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  is empty ; ::_thesis: verum
end;
then reconsider M9 =  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  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; ::_thesis: ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) )
now__::_thesis:_(_CP_in_M9_implies_(_(ObjectDerivation_C)_._the_Extent_of_CP_=_the_Intent_of_CP_&_(AttributeDerivation_C)_._the_Intent_of_CP_=_the_Extent_of_CP_)_)
assume  CP in M9 ; ::_thesis: ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP )
then  ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is 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 ) ; ::_thesis: verum
end;
hence  ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ) ; ::_thesis: verum
end;
hence   {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  is non empty set ; ::_thesis: verum
end;
end;

:: deftheorem  defines B-carrier CONLAT_1:def_17_:_
 for C being FormalContext holds B-carrier C =  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  ;

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

registration
let C be FormalContext;
cluster B-carrier C ->  non empty ;
coherence
 not B-carrier C is empty ;
end;

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

definition
let C be FormalContext;
func B-meet C ->  BinOp of (B-carrier C) means :Def18: :: CONLAT_1:def 18
 for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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
 ex b1 being BinOp of (B-carrier C) st
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . (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
defpred S1[ FormalConcept of C, FormalConcept of C, set ] means  ex O being Subset of the carrier of C ex 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, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
proof
let CP1, CP2 be Element of B-carrier C; ::_thesis: ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
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(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #);
A2: (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) = (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 Def10
.= the Extent of CP1 /\ the Extent of CP2 by Def10 ;
then A3: (ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2) = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) by Th7;
then  not ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) is empty by Lm1;
then  ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) in  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  by A2, A3;
hence  ex CP being Element of B-carrier C st S1[CP1,CP2,CP] ; ::_thesis: verum
end;
consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that
A4: for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)] from BINOP_1:sch_3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
take  f ; ::_thesis: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) )
 for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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; ::_thesis: ex O being Subset of the carrier of C ex 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)) )
 ( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th31;
hence  ex O being Subset of the carrier of C ex 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)) ) by A4; ::_thesis: verum
end;
hence  for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (B-carrier C) st ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . (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)) ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . (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)) ) ) holds
b1 = b2
proof
let F1, F2 be BinOp of (B-carrier C); ::_thesis: ( ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ) implies F1 = F2 )
assume A5: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ; ::_thesis: ( ex CP1, CP2 being strict FormalConcept of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = the Extent of CP1 /\ the Extent of CP2 or not A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) or F1 = F2 )
assume A6: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) ) ; ::_thesis: F1 = F2
A7: for X being set st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X
proof
let X be set ; ::_thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume  X in [:(B-carrier C),(B-carrier C):] ; ::_thesis: F1 . X = F2 . X
then consider A, B being set  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 = B as strict FormalConcept of C by A9, Th31;
reconsider A = A as strict FormalConcept of C by A8, Th31;
 ( ex O being Subset of the carrier of C ex 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 ex 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  F1 . X = F2 . X by A10; ::_thesis: verum
end;
 ( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def_1;
hence  F1 = F2 by A7, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def18 defines B-meet CONLAT_1:def_18_:_
 for C being FormalContext
for b2 being BinOp of (B-carrier C) holds
( b2 = B-meet C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . (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)) ) );

definition
let C be FormalContext;
func B-join C ->  BinOp of (B-carrier C) means :Def19: :: CONLAT_1:def 19
 for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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
 ex b1 being BinOp of (B-carrier C) st
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . (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
defpred S1[ FormalConcept of C, FormalConcept of C, set ] means  ex O being Subset of the carrier of C ex 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, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
proof
let CP1, CP2 be Element of B-carrier C; ::_thesis: ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
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(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #);
A2: (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) = (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 Def10
.= the Intent of CP1 /\ the Intent of CP2 by Def10 ;
then  ( (AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2) = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & not ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #) is empty ) by Lm1, Th7;
then  ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #) in  {  ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E )  }  by A2;
hence  ex CP being Element of B-carrier C st S1[CP1,CP2,CP] ; ::_thesis: verum
end;
consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that
A3: for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)] from BINOP_1:sch_3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
take  f ; ::_thesis: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 )
 for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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; ::_thesis: ex O being Subset of the carrier of C ex 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 )
 ( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th31;
hence  ex O being Subset of the carrier of C ex 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 ) by A3; ::_thesis: verum
end;
hence  for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (B-carrier C) st ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . (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 ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . (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 ) ) holds
b1 = b2
proof
let F1, F2 be BinOp of (B-carrier C); ::_thesis: ( ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ) implies F1 = F2 )
assume A4: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ; ::_thesis: ( ex CP1, CP2 being strict FormalConcept of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) or not A = the Intent of CP1 /\ the Intent of CP2 ) or F1 = F2 )
assume A5: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 ) ; ::_thesis: F1 = F2
A6: for X being set st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X
proof
let X be set ; ::_thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume  X in [:(B-carrier C),(B-carrier C):] ; ::_thesis: F1 . X = F2 . X
then consider A, B being set  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 = B as strict FormalConcept of C by A8, Th31;
reconsider A = A as strict FormalConcept of C by A7, Th31;
 ( ex O being Subset of the carrier of C ex 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 ex 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  F1 . X = F2 . X by A9; ::_thesis: verum
end;
 ( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def_1;
hence  F1 = F2 by A6, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines B-join CONLAT_1:def_19_:_
 for C being FormalContext
for b2 being BinOp of (B-carrier C) holds
( b2 = B-join C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . (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 ) );

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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) in rng (B-meet C)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,CP2) in rng (B-meet 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  (B-meet C) . (CP1,CP2) in rng (B-meet C) by FUNCT_1:def_3; ::_thesis: verum
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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,CP2) in rng (B-join 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  (B-join C) . (CP1,CP2) in rng (B-join C) by FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th32: :: CONLAT_1:32
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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1)
 ( ex O being Subset of the carrier of C ex 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 ex 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 Def18;
hence  (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1) ; ::_thesis: verum
end;

theorem Th33: :: CONLAT_1:33
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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)
 ( ex O being Subset of the carrier of C ex 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 ex 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 Def19;
hence  (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1) ; ::_thesis: verum
end;

theorem Th34: :: CONLAT_1:34
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; ::_thesis: 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)
let CP1, CP2, CP3 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)
 (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 ex 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 ex 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 Def18;
 (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 ex 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 ex 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 Def18;
(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  (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; ::_thesis: verum
end;

theorem Th35: :: CONLAT_1:35
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; ::_thesis: 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)
let CP1, CP2, CP3 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3)
 (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 ex 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 ex 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 Def19;
 (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 ex 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 ex 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 Def19;
(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  (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; ::_thesis: verum
end;

theorem Th36: :: CONLAT_1:36
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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2
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 ex 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 ex 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 Def18, Def19;
 (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 Def10
.= the Extent of CP2 by Def10 ;
((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 Def10
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ the Intent of CP2 by Def10
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2) by Def10
.= (ObjectDerivation C) . the Extent of CP2 by A1, Th3, XBOOLE_1:28
.= the Intent of CP2 by Def10 ;
hence  (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2 by A2, A3; ::_thesis: verum
end;

theorem Th37: :: CONLAT_1:37
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; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1
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 ex 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 ex 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 Def18, Def19;
 (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 Def10
.= the Intent of CP1 by Def10 ;
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 Def10
.= the Extent of CP1 /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2)) by Def10
.= ((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2)) by Def10
.= (AttributeDerivation C) . the Intent of CP1 by A1, Th4, XBOOLE_1:28
.= the Extent of CP1 by Def10 ;
hence  (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1 by A2, A3; ::_thesis: verum
end;

theorem :: CONLAT_1:38
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; ::_thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP
let CP be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP
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 Def18;
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, Def10
.= (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, Def10
.= (ObjectDerivation C) . the Extent of CP by Th7
.= the Intent of CP by Def10 ;
hence  (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP by A1, A4; ::_thesis: verum
end;

theorem Th39: :: CONLAT_1:39
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; ::_thesis: for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C
let CP be strict FormalConcept of C; ::_thesis: (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects 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 Def19;
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 Def10
.= the Extent of (Concept-with-all-Objects C) by Def10 ;
A = ((ObjectDerivation C) . the Extent of CP) /\ the Intent of (Concept-with-all-Objects C) by A3, Def10
.= ((ObjectDerivation C) . the Extent of CP) /\ ((ObjectDerivation C) . the Extent of (Concept-with-all-Objects C)) by Def10
.= (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 Def10 ;
hence  (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C by A1, A4; ::_thesis: verum
end;

theorem :: CONLAT_1:40
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; ::_thesis: for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP
let CP be strict FormalConcept of C; ::_thesis: (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP
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 Def19;
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, Def10
.= (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, Def10
.= (AttributeDerivation C) . the Intent of CP by Th8
.= the Extent of CP by Def10 ;
hence  (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP by A1, A4; ::_thesis: verum
end;

theorem :: CONLAT_1:41
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; ::_thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C
let CP be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes 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 Def18;
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 Def10
.= the Intent of (Concept-with-all-Attributes C) by Def10 ;
O = ((AttributeDerivation C) . the Intent of CP) /\ the Extent of (Concept-with-all-Attributes C) by A2, Def10
.= ((AttributeDerivation C) . the Intent of CP) /\ ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Def10
.= (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 Def10 ;
hence  (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C by A1, A4; ::_thesis: verum
end;

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

:: deftheorem  defines ConceptLattice CONLAT_1:def_20_:_
 for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

theorem Th42: :: CONLAT_1:42
for C being FormalContext holds ConceptLattice C is Lattice
proof
let C be FormalContext; ::_thesis: ConceptLattice C is Lattice
set L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);
reconsider L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) as non empty strict 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; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider b = b, c = c as Element of B-carrier C ;
reconsider d = (B-join C) . (b,c) as Element of L ;
reconsider b = b, c = c as Element of L ;
reconsider a = a, b = b as Element of B-carrier C ;
reconsider e = (B-join C) . (a,b) as Element of L ;
reconsider a = a, b = 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 = a, b = b, c = 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  a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, A3; ::_thesis: verum
end;
A4: for a, b being Element of L holds (a "/\" b) "\/" b = b
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
reconsider a = a, b = b as Element of B-carrier C ;
reconsider d = (B-meet C) . (a,b) as Element of L ;
reconsider a = a, b = 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 = a, b = b as strict FormalConcept of C by Th31;
 (B-join C) . (((B-meet C) . (a,b)),b) = b by Th36;
hence  (a "/\" b) "\/" b = b by A5; ::_thesis: verum
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; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider b = b, c = c as Element of B-carrier C ;
reconsider d = (B-meet C) . (b,c) as Element of L ;
reconsider b = b, c = 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 = a, b = b as Element of B-carrier C ;
reconsider e = (B-meet C) . (a,b) as Element of L ;
reconsider a = a, b = 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 = a, b = b, c = 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  a "/\" (b "/\" c) = (a "/\" b) "/\" c by A7, A8; ::_thesis: verum
end;
A9: for a, b being Element of L holds a "/\" b = b "/\" a
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
A10: b "/\" a = (B-meet C) . (b,a) by LATTICES:def_2;
reconsider a = a, b = b as strict FormalConcept of C by Th31;
 (B-meet C) . (a,b) = (B-meet C) . (b,a) by Th32;
hence  a "/\" b = b "/\" a by A10, LATTICES:def_2; ::_thesis: verum
end;
A11: for a, b being Element of L holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a
reconsider a = a, b = b as Element of B-carrier C ;
reconsider d = (B-join C) . (a,b) as Element of L ;
reconsider a = a, b = 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 = a, b = b as strict FormalConcept of C by Th31;
 (B-meet C) . (a,((B-join C) . (a,b))) = a by Th37;
hence  a "/\" (a "\/" b) = a by A12; ::_thesis: verum
end;
 for a, b being Element of L holds a "\/" b = b "\/" a
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
A13: b "\/" a = (B-join C) . (b,a) by LATTICES:def_1;
reconsider a = a, b = b as strict FormalConcept of C by Th31;
 (B-join C) . (a,b) = (B-join C) . (b,a) by Th33;
hence  a "\/" b = b "\/" a by A13, LATTICES:def_1; ::_thesis: verum
end;
then  ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A1, A4, A9, A6, A11, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  ConceptLattice C is Lattice ; ::_thesis: verum
end;

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

definition
let C be FormalContext;
let S be non empty Subset of (ConceptLattice C);
:: original: Element
redefine mode Element of S ->  FormalConcept of C;
coherence
 for b1 being Element of S holds b1 is FormalConcept of C
proof
let s be Element of S; ::_thesis: s is FormalConcept of C
 s is Element of B-carrier C ;
hence  s is FormalConcept of C ; ::_thesis: verum
end;
end;

definition
let C be FormalContext;
let CP be Element of (ConceptLattice C);
funcCP @  ->  strict FormalConcept of C equals :: CONLAT_1:def 21
CP;
coherence
 CP is strict FormalConcept of C by Th31;
end;

:: deftheorem  defines @ CONLAT_1:def_21_:_
 for C being FormalContext
for CP being Element of (ConceptLattice C) holds CP @ = CP;

theorem Th43: :: CONLAT_1:43
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; ::_thesis: for CP1, CP2 being Element of (ConceptLattice C) holds
( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
let CP1, CP2 be Element of (ConceptLattice C); ::_thesis: ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
set CL = ConceptLattice C;
A1: now__::_thesis:_(_CP1_@_is-SubConcept-of_CP2_@_implies_CP1_[=_CP2_)
assume A2: CP1 @ is-SubConcept-of CP2 @ ; ::_thesis: CP1 [= 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 Def19;
 the Extent of (CP1 @) c= the Extent of (CP2 @) by A2, Def16;
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, Def10
.= the Extent of (CP2 @) by Def10 ;
then  CP1 "\/" CP2 = CP2 by A3, A4, A6, LATTICES:def_1;
hence  CP1 [= CP2 by LATTICES:def_3; ::_thesis: verum
end;
now__::_thesis:_(_CP1_[=_CP2_implies_CP1_@_is-SubConcept-of_CP2_@_)
assume  CP1 [= CP2 ; ::_thesis: CP1 @ is-SubConcept-of CP2 @
then  CP1 "\/" CP2 = CP2 by LATTICES:def_3;
then A7: the L_join of (ConceptLattice C) . (CP1,CP2) = CP2 by LATTICES:def_1;
 ex O being Subset of the carrier of C ex 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 Def19;
then  for x being set st x in the Intent of (CP2 @) holds
x in the Intent of (CP1 @) by A7, XBOOLE_0:def_4;
then  the Intent of (CP2 @) c= the Intent of (CP1 @) by TARSKI:def_3;
hence  CP1 @ is-SubConcept-of CP2 @ by Th28; ::_thesis: verum
end;
hence  ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ ) by A1; ::_thesis: verum
end;

theorem Th44: :: CONLAT_1:44
for C being FormalContext holds ConceptLattice C is complete Lattice
proof
let C be FormalContext; ::_thesis: ConceptLattice C is complete Lattice
 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); ::_thesis: 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 ) )
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: 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 ) )
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); ::_thesis: ( b is_less_than X implies b [= Top (ConceptLattice C) )
assume  b is_less_than X ; ::_thesis: b [= Top (ConceptLattice C)
 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); ::_thesis: ( CO "\/" CP = CO & CP "\/" CO = CO )
reconsider CP = CP as strict FormalConcept of C by Th31;
reconsider CO = CO as strict FormalConcept of C ;
(B-join C) . (CO,CP) = (B-join C) . (CP,CO) by Th33
.= CO by Th39 ;
hence  ( CO "\/" CP = CO & CP "\/" CO = CO ) by LATTICES:def_1; ::_thesis: verum
end;
hence  ex c being Element of (ConceptLattice C) st
for a being Element of (ConceptLattice C) holds
( c "\/" a = c & a "\/" c = c ) ; ::_thesis: verum
end;
then  ConceptLattice C is upper-bounded by LATTICES:def_14;
then  (Top (ConceptLattice C)) "\/" b = Top (ConceptLattice C) ;
hence  b [= Top (ConceptLattice C) by LATTICES:def_3; ::_thesis: verum
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  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 ) ) by A2; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: 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 ) )
then reconsider X = 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  {  the Extent of x where x is Element of B-carrier C : x in X  }
proof
let x be Element of X; ::_thesis: the Extent of x in  {  the Extent of x where x is Element of B-carrier C : x in X  }
 x in X ;
then reconsider x = x as Element of B-carrier C ;
 the Extent of x in  {  the Extent of x where x is Element of B-carrier C : x in X  }  ;
hence  the Extent of x in  {  the Extent of x where x is Element of B-carrier C : x in X  }  ; ::_thesis: verum
end;
then reconsider ExX =  {  the Extent of x where x is Element of B-carrier C : x in X  }  as non empty set ;
set E1 = meet ExX;
A4: for o being Object of C holds
( o in meet ExX iff for x being Element of X holds o in the Extent of x )
proof
let o be Object of C; ::_thesis: ( o in meet ExX iff for x being Element of X holds o in the Extent of x )
A5: ( ( for x being Element of X holds o in the Extent of x ) implies o in meet ExX )
proof
assume A6: for x being Element of X holds o in the Extent of x ; ::_thesis: o in meet ExX
 for Y being set st Y in ExX holds
o in Y
proof
let Y be set ; ::_thesis: ( Y in ExX implies o in Y )
assume  Y in ExX ; ::_thesis: o in Y
then  ex Y9 being Element of B-carrier C st
( Y = the Extent of Y9 & Y9 in X ) ;
hence  o in Y by A6; ::_thesis: verum
end;
hence  o in meet ExX by SETFAM_1:def_1; ::_thesis: verum
end;
 ( o in meet ExX implies for x being Element of X holds o in the Extent of x )
proof
assume A7: o in meet ExX ; ::_thesis: for x being Element of X holds o in the Extent of x
let x be Element of X; ::_thesis: o in the Extent of x
 the Extent of x in ExX by A3;
hence  o in the Extent of x by A7, SETFAM_1:def_1; ::_thesis: verum
end;
hence  ( o in meet ExX iff for x being Element of X holds o in the Extent of x ) by A5; ::_thesis: verum
end;
 meet ExX c= the carrier of C
proof
set Y = the Element of ExX;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet ExX or x in the carrier of C )
 the Element of ExX in ExX ;
then consider Y9 being Element of B-carrier C such that
A8: the Element of ExX = the Extent of Y9 and
 Y9 in X ;
assume  x in meet ExX ; ::_thesis: x in the carrier of C
then  x in the Extent of Y9 by A8, SETFAM_1:def_1;
hence  x in the carrier of C ; ::_thesis: verum
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  {  the Intent of x where x is Element of B-carrier C : x in X  }  ;
A10: for a being Attribute of C holds
( a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  iff ex x being Element of X st a in the Intent of x )
proof
let a be Attribute of C; ::_thesis: ( a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  iff ex x being Element of X st a in the Intent of x )
A11: ( ex x being Element of X st a in the Intent of x implies a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  )
proof
assume A12: ex x being Element of X st a in the Intent of x ; ::_thesis: a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }
 ex Y being set st
( a in Y & Y in  {  the Intent of x where x is Element of B-carrier C : x in X  }  )
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  {  the Intent of x where x is Element of B-carrier C : x in X  }  ;
hence  ex Y being set st
( a in Y & Y in  {  the Intent of x where x is Element of B-carrier C : x in X  }  ) by A13; ::_thesis: verum
end;
hence  a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  by TARSKI:def_4; ::_thesis: verum
end;
 ( a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  implies ex x being Element of X st a in the Intent of x )
proof
assume  a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  ; ::_thesis: ex x being Element of X st a in the Intent of x
then consider Y being set  such that
A14: a in Y and
A15: Y in  {  the Intent of x where x is Element of B-carrier C : x in X  }  by TARSKI:def_4;
 ex Y9 being Element of B-carrier C st
( Y = the Intent of Y9 & Y9 in X ) by A15;
hence  ex x being Element of X st a in the Intent of x by A14; ::_thesis: verum
end;
hence  ( a in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  iff ex x being Element of X st a in the Intent of x ) by A11; ::_thesis: verum
end;
 union  {  the Intent of x where x is Element of B-carrier C : x in X  }  c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  or x in the carrier' of C )
assume  x in union  {  the Intent of x where x is Element of B-carrier C : x in X  }  ; ::_thesis: x in the carrier' of C
then consider Y being set  such that
A16: x in Y and
A17: Y in  {  the Intent of x where x is Element of B-carrier C : x in X  }  by TARSKI:def_4;
 ex Y9 being Element of B-carrier C st
( Y = the Intent of Y9 & Y9 in X ) by A17;
hence  x in the carrier' of C by A16; ::_thesis: verum
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; ::_thesis: ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )
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 ; ::_thesis: o in O
 for x being Element of X holds o in the Extent of x
proof
let x be Element of X; ::_thesis: o in the Extent of x
 o in (AttributeDerivation C) . the Intent of x by A21;
hence  o in the Extent of x by Def10; ::_thesis: verum
end;
hence  o in O by A9; ::_thesis: verum
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 ; ::_thesis: for x being Element of X holds o in (AttributeDerivation C) . the Intent of x
 for x being Element of X holds o in (AttributeDerivation C) . the Intent of x
proof
let x be Element of X; ::_thesis: o in (AttributeDerivation C) . the Intent of x
 o in the Extent of x by A9, A22;
hence  o in (AttributeDerivation C) . the Intent of x by Def10; ::_thesis: verum
end;
hence  for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ; ::_thesis: verum
end;
hence  ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) by A20; ::_thesis: verum
end;
A23: for x being set st x in (AttributeDerivation C) . A9 holds
x in O
proof
let x be set ; ::_thesis: ( x in (AttributeDerivation C) . A9 implies x in O )
assume  x in (AttributeDerivation C) . A9 ; ::_thesis: x in O
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 Def4;
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; ::_thesis: x9 in (AttributeDerivation C) . the Intent of x
 for a being Attribute of C st a in the Intent of x holds
x9 is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in the Intent of x implies x9 is-connected-with a )
assume  a in the Intent of x ; ::_thesis: x9 is-connected-with a
then  a in A9 by A18;
hence  x9 is-connected-with a by A25; ::_thesis: verum
end;
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  x9 in (AttributeDerivation C) . the Intent of x by Def4; ::_thesis: verum
end;
hence  x in O by A19, A24; ::_thesis: verum
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 set st x in O holds
x in (AttributeDerivation C) . A9
proof
let x9 be set ; ::_thesis: ( x9 in O implies x9 in (AttributeDerivation C) . A9 )
assume A27: x9 in O ; ::_thesis: x9 in (AttributeDerivation C) . A9
then reconsider x9 = 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; ::_thesis: ( a in A9 implies x9 is-connected-with a )
assume  a in A9 ; ::_thesis: x9 is-connected-with a
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 Def4;
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  x9 is-connected-with a by A28; ::_thesis: verum
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  x9 in (AttributeDerivation C) . A9 by Def4; ::_thesis: verum
end;
then  O = (AttributeDerivation C) . A9 by A23, TARSKI:1;
then  ConceptStr(# O,A #) is FormalConcept of C by A26, Th21;
then reconsider p = ConceptStr(# O,A #) 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); ::_thesis: ( b is_less_than X implies b [= p )
assume A30: b is_less_than X ; ::_thesis: b [= p
 the Extent of (b @) c= the Extent of (p @)
proof
let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in the Extent of (b @) or x9 in the Extent of (p @) )
assume A31: x9 in the Extent of (b @) ; ::_thesis: x9 in the Extent of (p @)
then reconsider x9 = 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; ::_thesis: x9 in the Extent of x
 x in X ;
then reconsider x = 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 @) by Def16;
hence  x9 in the Extent of x by A31; ::_thesis: verum
end;
hence  x9 in the Extent of (p @) by A9; ::_thesis: verum
end;
then  b @ is-SubConcept-of p @ by Def16;
hence  b [= p by Th43; ::_thesis: verum
end;
 for q being Element of (ConceptLattice C) st q in X holds
p [= q
proof
let q be Element of (ConceptLattice C); ::_thesis: ( q in X implies p [= q )
assume A32: q in X ; ::_thesis: p [= q
 the Extent of (p @) c= the Extent of (q @)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of (p @) or x in the Extent of (q @) )
assume  x in the Extent of (p @) ; ::_thesis: x in the Extent of (q @)
hence  x in the Extent of (q @) by A9, A32; ::_thesis: verum
end;
then  p @ is-SubConcept-of q @ by Def16;
hence  p [= q by Th43; ::_thesis: verum
end;
then  p is_less_than X by LATTICE3:def_16;
hence  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 ) ) by A29; ::_thesis: verum
end;
end;
end;
hence  ConceptLattice C is complete Lattice by VECTSP_8:def_6; ::_thesis: verum
end;

registration
let C be FormalContext;
cluster ConceptLattice C ->  non empty strict complete ;
coherence
 ConceptLattice C is complete by Th44;
end;