reconsider O = the Intent of CP as Subset of the carrier of (C .:) ;
reconsider A = the Extent of CP as Subset of the carrier' of (C .:) ;
set CPD = ConceptStr(# O,A #);
A1: (AttributeDerivation (C .:)) . the Intent of ConceptStr(# O,A #) = (ObjectDerivation C) . the Extent of CP by Th18
.= the Extent of ConceptStr(# O,A #) by CONLAT_1:def 10 ;
A2: ConceptStr(# O,A #) = CP .: by Def8;
(ObjectDerivation (C .:)) . the Extent of ConceptStr(# O,A #) = (AttributeDerivation C) . the Intent of CP by Th19
.= the Intent of ConceptStr(# O,A #) by CONLAT_1:def 10 ;
hence ( not CP .: is empty & CP .: is concept-like ) by A1, A2, Lm3, CONLAT_1:def 10; :: thesis: verum