let C be FormalContext; :: thesis: for CP being strict FormalConcept of C holds
( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) )
let CP be strict FormalConcept of C; :: thesis: ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects 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;

A3: now :: thesis: ( the Intent of CP = {} implies CP = Concept-with-all-Objects C )

assume A4: the Intent of CP = {} ; :: thesis: CP = Concept-with-all-Objects C
then the Extent of CP = the carrier of C by A1, Th18;
then CP is universal ;
hence CP = Concept-with-all-Objects C by A2, A1, A4, Def12; :: thesis: verum

end;

now :: thesis: ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C )

assume A5: the Extent of CP = {} ; :: thesis: CP = Concept-with-all-Attributes C
then the Intent of CP = the carrier' of C by A2, Th17;
then CP is co-universal ;
hence CP = Concept-with-all-Attributes C by A2, A1, A5, Def13; :: thesis: verum

end;

hence ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) ) by A3; :: thesis: verum