CONLAT

:: CONLAT_2 semantic presentation

begin

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;
let CP be ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) ;

func @ CP -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) equals :: CONLAT_2:def 1
CP : ( ( ) ( ) ConceptStr over C : ( ( ) ( ) 2-sorted ) ) ;

end;

registration

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;

cluster ConceptLattice C : ( ( non quasi-empty ) ( non quasi-empty ) ContextStr ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) -> non empty strict bounded ;

end;

theorem :: CONLAT_2:1

theorem :: CONLAT_2:2

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for D being ( ( non empty ) ( non empty ) Subset-Family of ) holds (ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (union D : ( ( non empty ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = meet { ((ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) where O is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) } : ( ( ) ( ) set ) ;

theorem :: CONLAT_2:3

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for D being ( ( non empty ) ( non empty ) Subset-Family of ) holds (AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (union D : ( ( non empty ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = meet { ((AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) where A is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) } : ( ( ) ( ) set ) ;

theorem :: CONLAT_2:4

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;
let D be ( ( ) ( ) Subset of ) ;

func "/\" (D,C) -> ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of C : ( ( ) ( ) set ) ) equals :: CONLAT_2:def 2
"/\" (D : ( ( ) ( ) set ) ,(ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) ;

func "\/" (D,C) -> ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of C : ( ( ) ( ) set ) ) equals :: CONLAT_2:def 3
"\/" (D : ( ( ) ( ) set ) ,(ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: CONLAT_2:5

theorem :: CONLAT_2:6

theorem :: CONLAT_2:7

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for D being ( ( non empty ) ( non empty ) Subset of ) holds
( the Extent of ("\/" (D : ( ( non empty ) ( non empty ) Subset of ) ,C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) )) : ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = (AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (union { the Extent of ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where E is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) , I is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) in D : ( ( non empty ) ( non empty ) Subset of ) } ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & the Intent of ("\/" (D : ( ( non empty ) ( non empty ) Subset of ) ,C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) )) : ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = meet { the Intent of ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where E is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) , I is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) in D : ( ( non empty ) ( non empty ) Subset of ) } : ( ( ) ( ) set ) ) ;

theorem :: CONLAT_2:8

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for D being ( ( non empty ) ( non empty ) Subset of ) holds
( the Extent of ("/\" (D : ( ( non empty ) ( non empty ) Subset of ) ,C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) )) : ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = meet { the Extent of ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where E is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) , I is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) in D : ( ( non empty ) ( non empty ) Subset of ) } : ( ( ) ( ) set ) & the Intent of ("/\" (D : ( ( non empty ) ( non empty ) Subset of ) ,C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) )) : ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = (ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (union { the Intent of ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where E is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) , I is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ConceptStr(# E : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,I : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) in D : ( ( non empty ) ( non empty ) Subset of ) } ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: CONLAT_2:9

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for CP being ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) holds "\/" ( { ConceptStr(# O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) where O is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) , A is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ex o being ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) st
( o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) in the Extent of CP : ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) } ,(ConceptLattice C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (ConceptLattice b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) : ( ( ) ( non empty ) set ) ) = CP : ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) ;

theorem :: CONLAT_2:10

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for CP being ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) holds "/\" ( { ConceptStr(# O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) where O is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) , A is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ex a being ( ( ) ( ) Attribute of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Attribute of ( ( ) ( non empty ) set ) ) in the Intent of CP : ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {a : ( ( ) ( ) Attribute of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {a : ( ( ) ( ) Attribute of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) } ,(ConceptLattice C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ) : ( ( ) ( ) Element of the carrier of (ConceptLattice b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) : ( ( ) ( non empty ) set ) ) = CP : ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) ;

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;

func gamma C -> ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V11( the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) Function-like V17( the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Function of the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) means :: CONLAT_2:def 4
for o being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex O being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ex A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st
( it : ( ( ) ( ) set ) . o : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) = ConceptStr(# O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over C : ( ( ) ( ) set ) ) & O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (AttributeDerivation C : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((ObjectDerivation C : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {o : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (ObjectDerivation C : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {o : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) );

end;

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;

func delta C -> ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V11( the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) Function-like V17( the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) Function of the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) means :: CONLAT_2:def 5
for a being ( ( ) ( ) Element of the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ex O being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ex A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st
( it : ( ( ) ( ) set ) . a : ( ( ) ( ) Element of the carrier' of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) = ConceptStr(# O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ConceptStr over C : ( ( ) ( ) set ) ) & O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (AttributeDerivation C : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {a : ( ( ) ( ) Element of the carrier' of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (ObjectDerivation C : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((AttributeDerivation C : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . {a : ( ( ) ( ) Element of the carrier' of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) );

end;

theorem :: CONLAT_2:11

theorem :: CONLAT_2:12

theorem :: CONLAT_2:13

begin

theorem :: CONLAT_2:14

definition

let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;

func Context L -> ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) equals :: CONLAT_2:def 6
ContextStr(# the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,(LattRel L : ( ( ) ( ) set ) ) : ( ( V17( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V89() V92() V96() ) ( V7() V10( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V11( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V17( the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total V89() V92() V96() ) Element of bool [: the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ContextStr ) ;

end;

theorem :: CONLAT_2:15

for L being ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) holds ConceptLattice (Context L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ,L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) are_isomorphic ;

theorem :: CONLAT_2:16

for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) holds
( L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is complete iff ex C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) st ConceptLattice C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) are_isomorphic ) ;

begin

registration

let L be ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) Lattice) ;

cluster L : ( ( non empty Lattice-like complete ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) .: : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -> strict complete ;

end;

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;

func C .: -> ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) equals :: CONLAT_2:def 7
ContextStr(# the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,( the Information of C : ( ( ) ( ) set ) : ( ( ) ( V7() V10( the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V11( the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of bool [: the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( V7() V10( the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) V11( the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) Element of bool [: the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) ContextStr ) ;

end;

theorem :: CONLAT_2:17

for C being ( ( non quasi-empty strict ) ( non quasi-empty strict ) FormalContext) holds (C : ( ( non quasi-empty strict ) ( non quasi-empty strict ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) .: : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) = C : ( ( non quasi-empty strict ) ( non quasi-empty strict ) FormalContext) ;

theorem :: CONLAT_2:18

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for O being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (ObjectDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (AttributeDerivation (C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . O : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: CONLAT_2:19

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext)
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds (AttributeDerivation C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (ObjectDerivation (C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V11( bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V17( bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Element of bool [:(bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier' of (b₁ : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;
let CP be ( ( ) ( ) ConceptStr over C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) ;

func CP .: -> ( ( strict ) ( strict ) ConceptStr over C : ( ( ) ( ) set ) .: : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) ) means :: CONLAT_2:def 8
( the Extent of it : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (C : ( ( ) ( ) set ) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the Intent of CP : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & the Intent of it : ( ( ) ( ) Element of bool the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier' of (C : ( ( ) ( ) set ) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the Extent of CP : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) );

end;

registration

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;
let CP be ( ( non empty concept-like ) ( non empty concept-like ) FormalConcept of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) ;

cluster CP : ( ( non empty concept-like ) ( non empty concept-like ) ConceptStr over C : ( ( non quasi-empty ) ( non quasi-empty ) ContextStr ) ) .: : ( ( strict ) ( strict ) ConceptStr over C : ( ( non quasi-empty ) ( non quasi-empty ) ContextStr ) .: : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) ) -> strict non empty concept-like ;

end;

theorem :: CONLAT_2:20

definition

let C be ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ;

func DualHomomorphism C -> ( ( ) ( non empty V7() V10( the carrier of ((ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) .:) : ( ( strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (ConceptLattice (C : ( ( ) ( ) set ) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) : ( ( ) ( non empty ) set ) ) Function-like V17( the carrier of ((ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) .:) : ( ( strict ) ( non empty strict ) LattStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of (ConceptLattice C : ( ( ) ( ) set ) ) : ( ( non empty strict ) ( non empty strict ) LattStr ) .: : ( ( strict ) ( non empty strict ) LattStr ) , ConceptLattice (C : ( ( ) ( ) set ) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ) means :: CONLAT_2:def 9
for CP being ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of C : ( ( ) ( ) set ) ) holds it : ( ( ) ( ) set ) . CP : ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( ) ( ) set ) = CP : ( ( strict non empty concept-like ) ( strict non empty concept-like ) FormalConcept of C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) .: : ( ( strict ) ( strict ) ConceptStr over C : ( ( ) ( ) set ) .: : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) ) ;

end;

theorem :: CONLAT_2:21

theorem :: CONLAT_2:22

for C being ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) holds ConceptLattice (C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) .:) : ( ( non quasi-empty strict ) ( non quasi-empty strict ) ContextStr ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) ,(ConceptLattice C : ( ( non quasi-empty ) ( non quasi-empty ) FormalContext) ) : ( ( non empty strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete ) LattStr ) .: : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete ) LattStr ) are_isomorphic ;