:: deftheorem defines ND_ex_1 NOMIN_1:def 8 :
for v, a being object holds ND_ex_1 (v,a) = v .--> a;