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