let CP be ConceptStr of C; :: thesis: CP is quasi-empty
( the Extent of CP is empty or the Intent of CP is empty )

proof

set x = the Element of the Extent of CP;
assume not the Extent of CP is empty ; :: thesis: the Intent of CP is empty
then A1: the Element of the Extent of CP in the Extent of CP ;
thus the Intent of CP is empty :: thesis: verum

proof

set x = the Element of the Intent of CP;
assume not the Intent of CP is empty ; :: thesis: contradiction
then the Element of the Intent of CP in the Intent of CP ;
hence contradiction by A1, Def2; :: thesis: verum

end;

end;

hence CP is quasi-empty by Def12; :: thesis: verum