let C be FormalContext; :: thesis:
let CP be quasi-empty ConceptStr over C; :: thesis:
assume CP is FormalConcept of C ; :: thesis:
then reconsider CP = CP as FormalConcept of C ;
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def9;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def9;

per cases by Def8;

case the Intent of CP is empty ; :: thesis:

then the Extent of CP = the carrier of C by A1, Th18;
hence CP is universal ; :: thesis:

end;

case the Extent of CP is empty ; :: thesis:

then the Intent of CP = the carrier' of C by A2, Th17;
hence CP is co-universal ; :: thesis:

end;

end;

end;

hence ( CP is universal or CP is co-universal ) ; :: thesis: