:: deftheorem defines psi CONLAT_1:def 6 :
for C being FormalContext holds psi C = AttributeDerivation C;