:: deftheorem defines ND_ex_3 NOMIN_1:def 10 :
for v, v1, a, a1 being object holds ND_ex_3 (v,v1,a,a1) = (v,v1) --> (a,a1);