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 strict 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) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) ; :: thesis: verum