:: deftheorem defines ND_ex_4 NOMIN_1:def 11 :
for v, v1, v2, a, a1 being object holds ND_ex_4 (v,v1,v2,a,a1) = (v,v1) --> (a,(v2 .--> a1));