theorem :: EUCLID_4:16

for n being Nat
for x being Element of REAL n holds
( |(x,x)| = 0 iff |.x.| = 0 )