theorem :: CONLAT_1:22

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