let C be FormalContext; :: thesis: for CP being quasi-empty ConceptStr over C holds
( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
let CP be quasi-empty ConceptStr over C; :: thesis: ( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
assume A1: CP is strict FormalConcept of C ; :: thesis: ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )

now :: thesis: ( ( the Intent of CP is empty & CP = Concept-with-all-Objects C ) or ( the Extent of CP is empty & CP = Concept-with-all-Attributes C ) )

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 = Concept-with-all-Objects C

hence CP = Concept-with-all-Objects C by A1, Th25; :: thesis: verum

end;

case the Extent of CP is empty ; :: thesis: CP = Concept-with-all-Attributes C

hence CP = Concept-with-all-Attributes C by A1, Th25; :: thesis: verum

end;

end;

end;

hence ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) ; :: thesis: verum