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 Def13;

A2: now

assume the Intent of CP = {} ; :: thesis: CP is universal
then the Extent of CP = the carrier of C by A1, Th19;
hence CP is universal by Def14; :: thesis: verum

end;

A3: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def13;

now

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

end;

hence ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) by A2; :: thesis: verum