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

proof

set M' = ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #);
(AttributeDerivation C) . the Intent of ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) = the Extent of ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) by Th8;
hence ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C by Def13, Lm1; :: thesis: verum

end;

for O' being Subset of the carrier of C
for A' being Subset of the carrier' of C st ConceptStr(# O',A' #) is FormalConcept of C & A c= A' holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A'

proof

let O' be Subset of the carrier of C; :: thesis: for A' being Subset of the carrier' of C st ConceptStr(# O',A' #) is FormalConcept of C & A c= A' holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A'
let A' be Subset of the carrier' of C; :: thesis: ( ConceptStr(# O',A' #) is FormalConcept of C & A c= A' implies (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A' )
assume A2: ( ConceptStr(# O',A' #) is FormalConcept of C & A c= A' ) ; :: thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A'
then reconsider M' = ConceptStr(# O',A' #) as FormalConcept of C ;
A3: (AttributeDerivation C) . A' = the Extent of M' by Def13
.= O' ;
A4: (ObjectDerivation C) . O' = the Intent of M' by Def13
.= A' ;
(AttributeDerivation C) . A' c= (AttributeDerivation C) . A by A2, Th4;
hence (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A' by A3, A4, Th3; :: thesis: verum

end;

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