:: 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 .: );