let C be FormalContext; :: thesis: for CP being quasi-empty ConceptStr of 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 of 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

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

hence CP = Concept-with-all-Objects C by A1, Th26; :: 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, Th26; :: thesis: verum

end;

end;

end;

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