let CP be ConceptStr of C; :: thesis: CP is empty
A1: the Extent of CP is empty ;
the Intent of CP is empty ;
hence CP is empty by A1, Def11; :: thesis: verum