:: deftheorem defines ND_ex_2 NOMIN_1:def 9 :
for v, v1, a1 being object holds ND_ex_2 (v,v1,a1) = v .--> (v1 .--> a1);