theorem :: CONLAT_1:20

for C being FormalContext
for O being Subset of the carrier of C holds
( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O )