:: Introduction to Concept Lattices
:: by Christoph Schwarzweller
::
:: Received October 2, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


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 )
proofend;
cluster strict non quasi-empty for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & not b1 is quasi-empty )
proofend;
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 )
proofend;
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 )
proofend;
cluster non quasi-empty strict for ContextStr ;
existence
 ex b1 being ContextStr st
( b1 is strict & not b1 is quasi-empty )
proofend;
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
proofend;
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
proofend;
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  }
proofend;
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
proofend;
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  }
proofend;
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
proofend;
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  }
proofend;

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  }
proofend;

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
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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))
proofend;

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))
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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)
proofend;
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)
proofend;
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) &amp; 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] &amp; f is antitone &amp; g is antitone &amp; ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) &amp; 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 ) )
proofend;

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) &amp; g = g * (f * g) )
proofend;

theorem :: CONLAT_1:14
for C being FormalContext holds [(phi C),(psi C)] is co-Galois
proofend;

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)
proofend;

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)
proofend;

theorem Th17: :: CONLAT_1:17
for C being FormalContext holds (ObjectDerivation C) . {} = the carrier' of C
proofend;

theorem Th18: :: CONLAT_1:18
for C being FormalContext holds (AttributeDerivation C) . {} = the carrier of C
proofend;

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 &amp; 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 &amp; 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 &amp; not b1 is empty )
proofend;
cluster strict quasi-empty for ConceptStr over C;
existence
 ex b1 being ConceptStr over C st
( b1 is strict &amp; b1 is quasi-empty )
proofend;
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
proofend;
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
proofend;
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
proofend;

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 &amp; (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 &amp; (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 &amp; not b1 is empty )
proofend;
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
proofend;
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 &amp; ( 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 &amp; O c= O9 holds
(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 ) )
proofend;

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 )
proofend;

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 &amp; ( 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 &amp; A c= A9 holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) )
proofend;

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 )
proofend;

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 &amp; b1 is universal )
proofend;
cluster strict non empty concept-like co-universal for ConceptStr over C;
existence
 ex b1 being FormalConcept of C st
( b1 is strict &amp; b1 is co-universal )
proofend;
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 #) &amp; O = (AttributeDerivation C) . {} &amp; 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 #) &amp; O = (AttributeDerivation C) . {} &amp; A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) )
proofend;
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 #) &amp; O = (AttributeDerivation C) . {} &amp; A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) &amp; ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) &amp; O = (AttributeDerivation C) . {} &amp; 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 #) &amp; O = (AttributeDerivation C) . {} &amp; 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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) &amp; 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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) &amp; A = (ObjectDerivation C) . {} )
proofend;
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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) &amp; A = (ObjectDerivation C) . {} ) &amp; ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) &amp; 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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) &amp; 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 &amp; the Intent of (Concept-with-all-Attributes C) = the carrier' of C )
proofend;

theorem :: CONLAT_1:24
for C being FormalContext
for CP being FormalConcept of C holds
( ( the Extent of CP = {} implies CP is co-universal ) &amp; ( the Intent of CP = {} implies CP is universal ) )
proofend;

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 ) &amp; ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;
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 )
proofend;

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 &amp; Concept-with-all-Attributes C is-SubConcept-of CP )
proofend;

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 &amp; (ObjectDerivation C) . E = I &amp; (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 &amp; (ObjectDerivation C) . E = I &amp; (AttributeDerivation C) . I = E )  }  is non empty set
proofend;
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 &amp; (ObjectDerivation C) . E = I &amp; (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
proofend;
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 )
proofend;

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 #) &amp; O = the Extent of CP1 /\ the Extent of CP2 &amp; 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 #) &amp; O = the Extent of CP1 /\ the Extent of CP2 &amp; A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) )
proofend;
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 #) &amp; O = the Extent of CP1 /\ the Extent of CP2 &amp; A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) ) &amp; ( 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 #) &amp; O = the Extent of CP1 /\ the Extent of CP2 &amp; A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) ) holds
b1 = b2
proofend;
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 #) &amp; O = the Extent of CP1 /\ the Extent of CP2 &amp; 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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) &amp; 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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) &amp; A = the Intent of CP1 /\ the Intent of CP2 )
proofend;
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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) &amp; A = the Intent of CP1 /\ the Intent of CP2 ) ) &amp; ( 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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) &amp; A = the Intent of CP1 /\ the Intent of CP2 ) ) holds
b1 = b2
proofend;
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 #) &amp; O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) &amp; 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)
proofend;

Lm3:  for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

registration
let C be FormalContext;
cluster ConceptLattice C ->  non empty strict Lattice-like ;
coherence
 ( ConceptLattice C is strict &amp; not ConceptLattice C is empty &amp; 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
proofend;
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 @ )
proofend;

theorem Th44: :: CONLAT_1:44
for C being FormalContext holds ConceptLattice C is complete Lattice
proofend;

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