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

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

end;

now

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