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 .:) ;
take ConceptStr(# O,A #) ; :: thesis: ( the Extent of ConceptStr(# O,A #) = the Intent of CP & the Intent of ConceptStr(# O,A #) = the Extent of CP )
thus ( the Extent of ConceptStr(# O,A #) = the Intent of CP & the Intent of ConceptStr(# O,A #) = the Extent of CP ) ; :: thesis: verum