theorem :: CONLAT_1:38

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