:: deftheorem defines BK_model BKMODEL2:def 1 :
BK_model = negative_conic (1,1,(- 1),0,0,0);