let C be FormalContext; :: thesis: 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 )
let A be Subset of the carrier' of C; :: thesis: ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )

A1: now :: thesis: ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C implies (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )

A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) by Th6;
then A2: for x being object st x in A holds
x in (ObjectDerivation C) . ((AttributeDerivation C) . A) ;
given O being Subset of the carrier of C such that A3: ConceptStr(# O,A #) is FormalConcept of C ; :: thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) = A
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A by A3, Th21;
then for x being object st x in (ObjectDerivation C) . ((AttributeDerivation C) . A) holds
x in A ;
hence (ObjectDerivation C) . ((AttributeDerivation C) . A) = A by A2, TARSKI:2; :: thesis: verum

end;

now :: thesis: ( (ObjectDerivation C) . ((AttributeDerivation C) . A) = A implies ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C )

reconsider O = (AttributeDerivation C) . A as Subset of the carrier of C ;
set M9 = ConceptStr(# O,A #);
assume (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ; :: thesis: ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C
then ConceptStr(# O,A #) is FormalConcept of C by Def9, Lm1;
hence ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C ; :: thesis: verum

end;

hence ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ) by A1; :: thesis: verum