theorem Th19: :: CONLAT_1:19

for C being FormalContext
for O being Subset of the carrier of C holds
( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C
for A9 being Subset of the carrier' of C st ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 holds
(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 ) )