:: deftheorem Def12 defines Concept-with-all-Objects CONLAT_1:def 13 :
for C being FormalContext
for b₂ being strict universal FormalConcept of C holds
( b₂ = Concept-with-all-Objects 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) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) );