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

proof

let O9 be Subset of the carrier of C; :: thesis: for A9 being Subset of the carrier' of C st ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 holds
(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9
let A9 be Subset of the carrier' of C; :: thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 implies (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 )
assume that
A2: ConceptStr(# O9,A9 #) is FormalConcept of C and
A3: O c= O9 ; :: thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9
reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2;
A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def9
.= O9 ;
A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def9
.= A9 ;
(ObjectDerivation C) . O9 c= (ObjectDerivation C) . O by A3, Th3;
hence (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 by A4, A5, Th4; :: thesis: verum

end;

ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C

proof

set M9 = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #);
(ObjectDerivation C) . the Extent of ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) = the Intent of ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) by Th7;
hence ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C by Def9, Lm1; :: thesis: verum

end;

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