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