theorem Th33: :: EUCLID_2:35

for n being Nat
for p being Point of (TOP-REAL n) holds |(p,p)| >= 0 by RVSUM_1:119;