:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def 9 :
for C being FormalContext
for b₂ being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) holds
( b₂ = DualHomomorphism C iff for CP being strict FormalConcept of C holds b₂ . CP = CP .: );