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 Th20;
(ObjectDerivation C) . {} = the carrier' of C by Th18;
then CP is co-universal by Def15;
hence ex b₁ being FormalConcept of C st
( b₁ is strict & b₁ is co-universal ) ; :: thesis: verum