:: deftheorem Def5 defines delta CONLAT_2:def 5 :
for C being FormalContext
for b₂ being Function of the carrier' of C, the carrier of (ConceptLattice C) holds
( b₂ = delta C iff for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) );