let C be FormalContext; :: thesis: for CP being quasi-empty ConceptStr over C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )
let CP be quasi-empty ConceptStr over 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 Def9;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def9;

now :: thesis: ( ( the Intent of CP is empty & CP is universal ) or ( the Extent of CP is empty & CP is co-universal ) )

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

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

then the Extent of CP = the carrier of C by A1, Th18;
hence CP is universal ; :: 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, Th17;
hence CP is co-universal ; :: thesis: verum

end;

end;

end;

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