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

proof

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

end;

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

proof

set M' = 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 Def13, Lm1; :: thesis: verum

end;

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