:: deftheorem defines universal CONLAT_1:def 11 :
for C being FormalContext
for CP being ConceptStr over C holds
( CP is universal iff the Extent of CP = the carrier of C );