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