let C be FormalContext; :: thesis: for CP being quasi-empty ConceptStr of C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )
let CP be quasi-empty ConceptStr of C; :: thesis: ( not CP is FormalConcept of C or CP is universal or CP is co-universal )
assume CP is FormalConcept of C ; :: thesis: ( CP is universal or CP is co-universal )
then reconsider CP = CP as FormalConcept of C ;
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def13;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def13;

now

per cases ( the Intent of CP is empty or the Extent of CP is empty ) by Def12;

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

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

end;

case the Extent of CP is empty ; :: thesis: CP is co-universal

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

end;

end;

end;

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