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: ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) by Def13;

A2: now

assume A3: the Extent of CP = {} ; :: thesis: CP = Concept-with-all-Attributes C
then the Intent of CP = the carrier' of C by A1, Th18;
then CP is co-universal by Def15;
hence CP = Concept-with-all-Attributes C by A1, A3, Def17; :: thesis: verum

end;

now

assume A4: the Intent of CP = {} ; :: thesis: CP = Concept-with-all-Objects C
then the Extent of CP = the carrier of C by A1, Th19;
then CP is universal by Def14;
hence CP = Concept-with-all-Objects C by A1, A4, Def16; :: 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 A2; :: thesis: verum