:: deftheorem defines B-carrier CONLAT_1:def 17 :
for C being FormalContext holds B-carrier C = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;