:: deftheorem defines lift_binary_pred NOMIN_4:def 7 :
for V, A being set
for a, b being Element of V
for p being Function of [:A,A:],BOOLEAN holds lift_binary_pred (p,a,b) = p * <:(denaming (V,A,a)),(denaming (V,A,b)):>;