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

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

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

end;

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

reconsider A = (ObjectDerivation C) . O as Subset of the carrier' of C ;
set M9 = ConceptStr(# O,A #);
assume (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ; :: thesis: ex A 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 A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C ; :: thesis: verum

end;

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