theorem :: CONLAT_2:20

for C being strict FormalContext
for CP being strict FormalConcept of C holds (CP .:) .: = CP