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 strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) ; :: thesis: verum