theorem :: CONLAT_1:40

for C being FormalContext
for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP