:: deftheorem defines Equality NOMIN_4:def 10 :
for V, A being set
for x, y being Element of V holds Equality (A,x,y) = lift_binary_pred ((Equality A),x,y);