let CP be ConceptStr of C; :: thesis: CP is empty
( the Extent of CP is empty & the Intent of CP is empty ) ;
hence CP is empty by Def11; :: thesis: verum