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 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 & A c= A9 holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) )
let A be Subset of the carrier' of C; :: thesis: ( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) 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 & A c= A9 holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) )
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 & A c= A9 holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9
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 & A c= A9 holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9
let A9 be Subset of the carrier' of C; :: thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & A c= A9 implies (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 )
assume that
A2: ConceptStr(# O9,A9 #) is FormalConcept of C and
A3: A c= A9 ; :: thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9
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 ;
(AttributeDerivation C) . A9 c= (AttributeDerivation C) . A by A3, Th4;
hence (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 by A4, A5, Th3; :: thesis: verum
end;
ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C
proof
set M9 = 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 Def9, Lm1; :: thesis: verum
end;
hence ( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) 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 & A c= A9 holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) ) by A1; :: thesis: verum