theorem :: EUCLID_4:19

for n being Nat
for x being Element of REAL n holds |((0* n),x)| = 0 by Th18;