set CP = the FormalConcept of C;
A1: ( (ObjectDerivation C) . the Extent of the FormalConcept of C = the Intent of the FormalConcept of C & (AttributeDerivation C) . the Intent of the FormalConcept of C = the Extent of the FormalConcept of C ) by Def9;
( not the Intent of the FormalConcept of C is empty or not the Extent of the FormalConcept of C is empty ) by Def7;
then ConceptStr(# the Extent of the FormalConcept of C, the Intent of the FormalConcept of C #) is FormalConcept of C by A1, Def7, Def9;
hence ex b₁ being FormalConcept of C st b₁ is strict ; :: thesis: verum