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

assume A2: (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ; :: thesis: 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 M' = ConceptStr(# O,A #);
ConceptStr(# O,A #) is FormalConcept of C by A2, Def13, Lm1;
hence ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C ; :: thesis: verum

end;

now

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, Th22;
then A4: for x being set st x in (ObjectDerivation C) . ((AttributeDerivation C) . A) holds
x in A ;
A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) by Th6;
then for x being set st x in A holds
x in (ObjectDerivation C) . ((AttributeDerivation C) . A) ;
hence (ObjectDerivation C) . ((AttributeDerivation C) . A) = A by A4, TARSKI:2; :: 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