:: deftheorem Def13 defines Concept-with-all-Attributes CONLAT_1:def 14 :
for C being FormalContext
for b₂ being strict co-universal FormalConcept of C holds
( b₂ = Concept-with-all-Attributes C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) );