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;
end;
end;
hence ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) ; :: thesis: verum