:: deftheorem defines phi CONLAT_1:def 5 :
for C being FormalContext holds phi C = ObjectDerivation C;