theorem :: CONLAT_1:41

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