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

assume A1: not the Extent of CP is empty ; :: thesis: the Intent of CP is empty
consider x being Element of the Extent of CP;
A2: x in the Extent of CP by A1;
thus the Intent of CP is empty :: thesis: verum

proof

assume A3: not the Intent of CP is empty ; :: thesis: contradiction
consider x being Element of the Intent of CP;
x in the Intent of CP by A3;
hence contradiction by A2, Def2; :: thesis: verum

end;

end;

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