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


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

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

:: deftheorem CONLAT_1:def 1 :
canceled;

registration
cluster non empty non void strict for ContextStr ;
existence
ex b1 being ContextStr st
( b1 is strict & not b1 is empty & not b1 is void )
proof end;
end;

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

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

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

registration
let C be non empty non void 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 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 end;
end;

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

:: deftheorem 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;

definition
let C be FormalContext;
func ObjectDerivation C -> Function of (bool the carrier of C),(bool the carrier' of C) means :Def2: :: 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 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 end;
end;

:: deftheorem Def2 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 :Def3: :: 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 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 end;
end;

:: deftheorem Def3 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 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 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 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 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 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 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 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 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 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 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 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 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 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;
attr Con is co-Galois means :: 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 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 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 end;

theorem :: CONLAT_1:14
for C being FormalContext holds [(phi C),(psi C)] is co-Galois
proof 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 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 end;

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

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

definition
let C be 2-sorted ;
attr c2 is strict ;
struct ConceptStr over C -> ;
aggr ConceptStr(# 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;
attr CP is empty means :Def7: :: CONLAT_1:def 8
( the Extent of CP is empty & the Intent of CP is empty );
attr CP is quasi-empty means :Def8: :: CONLAT_1:def 9
( the Extent of CP is empty or the Intent of CP is empty );
end;

:: deftheorem Def7 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 Def8 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 empty non void 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 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 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 ;
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 end;

definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is concept-like means :Def9: :: 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 Def9 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 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 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 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 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 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 end;

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

:: deftheorem 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;
attr CP is co-universal means :: CONLAT_1:def 12
 the Intent of CP = the carrier' of C;
end;

:: deftheorem 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 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 end;
end;

definition
let C be FormalContext;
func Concept-with-all-Objects C -> strict universal FormalConcept of C means :Def12: :: 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 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 Def12 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 :Def13: :: 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 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 Def13 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 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 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 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 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 end;

definition
let C be FormalContext;
mode Set-of-FormalConcepts of C -> non empty set means :Def14: :: 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 end;
end;

:: deftheorem Def14 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 Def14;
end;

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

:: deftheorem 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 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 end;

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 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 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 object holds
( CP in B-carrier C iff CP is strict FormalConcept of C )
proof end;

definition
let C be FormalContext;
func B-meet C -> BinOp of (B-carrier C) means :Def17: :: 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 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 end;
end;

:: deftheorem Def17 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 :Def18: :: 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 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 end;
end;

:: deftheorem Def18 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 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 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 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 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 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 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 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 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 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 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 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 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 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 end;
end;

definition
let C be FormalContext;
let CP be Element of (ConceptLattice C);
func CP @ -> 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 end;

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

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