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

A1: now

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

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

end;

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