theorem Th21: :: METRIC_1:21

for x, y being Element of 1 st x <> y holds
0 < Empty^2-to-zero . (x,y)