let C be FormalContext; :: thesis: for A being Subset of holds
( ex O being Subset of st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )
let A be Subset of ; :: thesis: ( ex O being Subset of st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )

A1: now

A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) by Th6;
then A2: for x being set st x in A holds
x in (ObjectDerivation C) . ((AttributeDerivation C) . A) ;
given O being Subset of 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 for x being set 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

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

end;

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