theorem :: METRIC_1:20

for x being set holds Empty^2-to-zero . (x,x) = 0