reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
reconsider CP = ConceptStr(# ((AttributeDerivation C) . e),((ObjectDerivation C) . ((AttributeDerivation C) . e)) #) as FormalConcept of C by Th21;
(AttributeDerivation C) . {} = the carrier of C by Th18;
then CP is universal ;
hence ex b₁ being FormalConcept of C st
( b₁ is strict & b₁ is universal ) ; :: thesis: verum