:: deftheorem Def2 defines ObjectDerivation CONLAT_1:def 3 :
for C being FormalContext
for b₂ being Function of (bool the carrier of C),(bool the carrier' of C) holds
( b₂ = ObjectDerivation C iff for O being Subset of the carrier of C holds b₂ . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } );