:: deftheorem defines @ CONLAT_2:def 1 :
for C being FormalContext
for CP being strict FormalConcept of C holds @ CP = CP;