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