let C be FormalContext; :: thesis: for CP being FormalConcept of C holds
( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )
let CP be FormalConcept of C; :: thesis: ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def9;
A2: ( the Intent of CP = {} implies CP is universal ) by A1, Th18;
A3: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def9;
( the Extent of CP = {} implies CP is co-universal ) by A3, Th17;
hence ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) by A2; :: thesis: verum