theorem Th5: :: ANPROJ11:5

for u being Element of (TOP-REAL 3) holds
( u is zero iff |(u,u)| = 0 )