:: deftheorem defines @ CONLAT_1:def 21 :
for C being FormalContext
for CP being Element of (ConceptLattice C) holds CP @ = CP;