theorem Th39: :: CONLAT_1:39

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